HighRankPaddingSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sum actual squarefree padding after the full high-rank column estimate.

lemma OAI.TwoPointCorrelations.weighted_pair_second_fiber_sum_le line 13

theorem OAI.TwoPointCorrelations.high_rank_column_padding_sum line 38

Source documentation

A complete reciprocal sum over numerical columns and numerical padding values. All pattern and padding catalogs are supplied by proved encodings, and the lit conditions are those of the original words.

theorem high_rank_column_padding_sum {J R : ℕ} (P : Fin J → Finset ℕ) (Qp : Finset ℕ)
    (F : Finset (ColumnPrimeAssignment J R P × (Fin R → ℕ)))
    (hR : 0 < R) (forward : Fin R → Bool) (j : Fin J)
    (h Q D B H r M : ℕ) (U : ℝ) (hU : 1 ≤ U)
    (hP : ∀ p ∈ P j, p.Prime) (hV : 0 < primeHarmonicMass (P j))
    (hmass : ∀ l, primeHarmonicMass (P l) ≤ U) (hQmass : primeHarmonicMass Qp ≤ U)
    (hH : 0 < H) (hlo : ∀ p ∈ P j, H ≤ p) (hbound : ∀ p ∈ P j, p ≤ B)
    (hq : ∀ a ∈ F, ∀ i, a.2 i ≤ Q)
    (hd : ∀ a ∈ F, ∀ i, (∏ l ∈ univ.erase j, (a.1 l i).val) ≤ D)
    (hsq : ∀ a ∈ F, ∀ i, Squarefree (a.2 i))
    (hpool : ∀ a ∈ F, ∀ i, (a.2 i).primeFactors ⊆ Qp)
    (hcount : ∀ a ∈ F, ∀ i, (a.2 i).primeFactors.card ≤ M)
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass