ReciprocalColumnRank.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite positive reciprocal majorant for one high-rank column.

theorem OAI.TwoPointCorrelations.ColumnWordPattern.reciprocal_high_rank_bound line 18

Source documentation

A single reciprocal factor is retained for each abstract label. The sum permits numerical collisions and is uniform in all fixed other-column data and the starting point of the word.

theorem reciprocal_high_rank_bound
    (w : ColumnWordPattern α) (h Q D B H : ℕ)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (hV : 0 < primeHarmonicMass P) (hH : 0 < H)
    (hlo : ∀ p ∈ P, H ≤ 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.primeHarmonicMass, OAI.TwoPointCorrelations.formalDeparture