OAI/NumberTheory/TwoPoint/Walks/HighRankWordEvents.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.column_difference_rank_probability line 16

   Source documentation

   Coefficient bounds supply the size hypothesis uniformly for every minor selected from the fixed column data.

   theorem column_difference_rank_probability
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
       (label : ℕ → α) (t : ℕ → ℤ) (left right : ρ → ℕ) (control : ρ → α)
       (hind : LinearIndependent ℝ (Sum.elim
         (fun i => formalDeparture label (fun a => (t a : ℝ)) (left i) -
           formalDeparture label (fun a => (t a : ℝ)) (right i))
         (fun i => Pi.basisFun ℝ α (control i))))
       (N T Q : ℕ) (hl : ∀ i, left i ≤ N) (hr : ∀ i, right i ≤ N)
       (ht : ∀ a < N, |t a| ≤ (T : ℤ)) (hQ : ∀ p ∈ P, p ≤ Q)
       (a : ℝ) (ha : 0 ≤ a) (hatom : ∀ p, μ.weight p ≤ a) :
       (FiniteLaw.independent (fun _ : α => μ)).probability (fun x =>
         ∀ i, ((x (control i)).val : ℤ) ∣
   …

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

2. theorem OAI.TwoPointCorrelations.high_rank_column_event_bound line 49

   Source documentation

   The high-rank probability saving only uses the chosen lit occurrences. The sampled word may vary with all primes in the column, while its integral step coefficients and selected indices remain fixed.

   theorem high_rank_column_event_bound
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
       (label : ℕ → α) (t : ℕ → ℤ) (left right : ρ → ℕ) (control : ρ → α)
       (hind : LinearIndependent ℝ (Sum.elim
         (fun i => formalDeparture label (fun a => (t a : ℝ)) (left i) -
           formalDeparture label (fun a => (t a : ℝ)) (right i))
         (fun i => Pi.basisFun ℝ α (control i))))
       (N T Q : ℕ) (hl : ∀ i, left i ≤ N) (hr : ∀ i, right i ≤ N)
       (ht : ∀ a < N, |t a| ≤ (T : ℤ)) (hQ : ∀ p ∈ P, p ≤ Q)
       (a : ℝ) (ha : 0 ≤ a) (hatom : ∀ p, μ.weight p ≤ a)
       (h : ℕ) (word : (α → P) → List SignedStep) (base : (α → P) → ℤ)
       (E : (α → P) → Prop)
   …

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