GoodColumnSum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Sum the good column patterns with one reciprocal per observed prime.

lemma OAI.TwoPointCorrelations.twice_observed_labels_le_slots_add_singletons line 15

Source documentation

Unused elements of the ambient label type make no contribution.

lemma twice_observed_labels_le_slots_add_singletons
    {ι τ : Type*} [Fintype ι] [Fintype τ] [DecidableEq ι] (label : τ → ι) :
    2 * (univ.image label).card ≤ Fintype.card τ + (singletonLabels label).card := by
…

Mentions: OAI.TwoPointCorrelations.singletonLabels

def OAI.TwoPointCorrelations.columnSingletonCount line 36
lemma OAI.TwoPointCorrelations.column_observed_count line 40
lemma OAI.TwoPointCorrelations.good_column_observed_count line 50
Source documentation
At most 2*S singleton labels leave at most J*k+S distinct primes in a word with 2*k occurrences per column.
```
lemma good_column_observed_count {J k S : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J (2 * k) P) (hs : columnSingletonCount w ≤ 2 * S) :
    (∑ j, (univ.image (w j)).card) ≤ J * k + S := by
…
```
Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.columnSingletonCount
theorem OAI.TwoPointCorrelations.covered_good_column_sum line 56

theorem OAI.TwoPointCorrelations.eventually_good_column_sum line 68

Source documentation

The universal forest decoder and the separate column masses give the required good-word prime sum. The exponential constant is absolute.

theorem eventually_good_column_sum :
    ∀ᶠ L : ℝ in atTop, ∀ J k S : ℕ, ∀ P : Fin J → Finset ℕ,
      ∀ F : Finset (ColumnPrimeAssignment J (2 * k) P), ∀ W : ℝ,
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 1 ≤ k → 1 ≤ W →
      (∀ j, primeHarmonicMass (P j) ≤ 2 * W) →
      (∀ w ∈ F, columnSingletonCount w ≤ 2 * S) →
      (∀ w ∈ F, ∃ c : BudgetColumnArrayCode J (4 * k) L,
        ∀ j i l, decodeBudgetColumnArray (show 2 * k ≤ 4 * k by omega) c j i l =
          decide (w j i = w j l)) →
      (∑ w ∈ F, columnReciprocalWeight w) ≤
        Real.exp (64 * k * J) * (2 * W) ^ (J * k + S) := by
…

Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.columnSingletonCount, OAI.TwoPointCorrelations.BudgetColumnArrayCode, OAI.TwoPointCorrelations.decodeBudgetColumnArray, OAI.TwoPointCorrelations.columnReciprocalWeight