OAI/NumberTheory/TwoPoint/Bounds/FixedColumnWords.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TwoPointCorrelations.ColumnWordPattern line 10
2. def OAI.TwoPointCorrelations.ColumnWordPattern.step line 21
3. def OAI.TwoPointCorrelations.ColumnWordPattern.word line 26
4. def OAI.TwoPointCorrelations.ColumnWordPattern.coefficient line 29
5. lemma OAI.TwoPointCorrelations.ColumnWordPattern.word_length line 32
6. lemma OAI.TwoPointCorrelations.ColumnWordPattern.displacement line 35
7. lemma OAI.TwoPointCorrelations.ColumnWordPattern.coefficient_abs line 42
8. lemma OAI.TwoPointCorrelations.ColumnWordPattern.coefficient_bound line 46
9. theorem OAI.TwoPointCorrelations.ColumnWordPattern.high_rank_event_bound line 56

   Source documentation

   The resampled step list has fixed coefficients independent of every numerical prime in the chosen column. Only selected departures need be lit.

   theorem high_rank_event_bound [Fintype α] [DecidableEq α]
       {ρ : Type*} [Fintype ρ] [DecidableEq ρ]
       (w : ColumnWordPattern α) (h Q D B : ℕ)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
       (hbound : ∀ p ∈ P, p ≤ B)
       (hq : ∀ j < w.length, w.padding j ≤ Q)
       (hd : ∀ j < w.length, w.otherColumns j ≤ D)
       (left right : ρ → ℕ) (control : ρ → α)
       (hl : ∀ i, left i ≤ w.length) (hr : ∀ i, right i ≤ w.length)
       (hind : LinearIndependent ℝ (Sum.elim
         (fun i => formalDeparture w.label (fun j => (w.coefficient h j : ℝ)) (left i) -
           formalDeparture w.label (fun j => (w.coefficient h j : ℝ)) (right i))
   …

   Mentions: OAI.TwoPointCorrelations.ColumnWordPattern, OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.formalDeparture