ColumnHarmonicSum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sum each column in its own prime pool after fixing the common pattern code.

abbrev OAI.TwoPointCorrelations.ColumnPrimeAssignment line 13
def OAI.TwoPointCorrelations.columnReciprocalWeight line 16
lemma OAI.TwoPointCorrelations.columnReciprocalWeight_nonneg line 20
theorem OAI.TwoPointCorrelations.same_column_patterns_reciprocal_sum line 25

theorem OAI.TwoPointCorrelations.covered_column_patterns_reciprocal_sum line 80

Source documentation

A code covers the joint pattern, but the numerical prime sums retain the separate harmonic mass of each column. There is no factor from the number of columns in the base of the power.

theorem covered_column_patterns_reciprocal_sum {J R : ℕ} {Code : Type*} [Fintype Code]
    (P : Fin J → Finset ℕ) (F : Finset (ColumnPrimeAssignment J R P))
    (decode : Code → Fin J → Fin R → Fin R → Bool) (A : ℝ) (M : ℕ)
    (hA : 1 ≤ A) (hmass : ∀ j, primeHarmonicMass (P j) ≤ A)
    (hlabels : ∀ w ∈ F, (∑ j, (univ.image (w j)).card) ≤ M)
    (hcover : ∀ w ∈ F, ∃ c, ∀ j i k, decode c j i k = decide (w j i = w j k)) :
    (∑ w ∈ F, columnReciprocalWeight w) ≤ (Fintype.card Code : ℝ) * A ^ M := by
…

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