GoodWordWeightedSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sum padding only after fixing each complete column pattern.

lemma OAI.TwoPointCorrelations.weighted_pair_sum_le line 13

theorem OAI.TwoPointCorrelations.covered_column_padding_sum line 43

Source documentation

The code may depend on the padding word. After fixing a code, sum all padding choices for each prime assignment and use the uniform bound. This avoids exchanging a prime-dependent cutoff with a supremum.

theorem covered_column_padding_sum {J R M : ℕ} {Q Code : Type*}
    [Fintype Q] [Fintype Code]
    (P : Fin J → Finset ℕ) (F : Finset (ColumnPrimeAssignment J R P × Q))
    (decode : Code → Fin J → Fin R → Fin R → Bool)
    (weight : ColumnPrimeAssignment J R P → Q → ℝ) (A K : ℝ)
    (hA : 1 ≤ A) (hK : 0 ≤ K)
    (hmass : ∀ j, primeHarmonicMass (P j) ≤ A)
    (hw : ∀ w q, 0 ≤ weight w q) (hpad : ∀ w, (∑ q, weight w q) ≤ K)
    (hlabels : ∀ a ∈ F, (∑ j, (univ.image (a.1 j)).card) ≤ M)
    (hcover : ∀ a ∈ F, ∃ c, ∀ j i l, decode c j i l = decide (a.1 j i = a.1 j l)) :
    (∑ a ∈ F, columnReciprocalWeight a.1 * weight a.1 a.2) ≤
      (Fintype.card Code : ℝ) * K * A ^ M := by
…

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

theorem OAI.TwoPointCorrelations.covered_good_column_padding_sum line 97

Source documentation

The good-word column count, with padding summed uniformly before the remaining prime assignments. All actual admissibility restrictions can remain in the finite set F.

theorem covered_good_column_padding_sum {J k S : ℕ} {Q Code : Type*}
    [Fintype Q] [Fintype Code]
    (P : Fin J → Finset ℕ) (F : Finset (ColumnPrimeAssignment J (2 * k) P × Q))
    (decode : Code → Fin J → Fin (2 * k) → Fin (2 * k) → Bool)
    (weight : ColumnPrimeAssignment J (2 * k) P → Q → ℝ) (A K : ℝ)
    (hA : 1 ≤ A) (hK : 0 ≤ K) (hmass : ∀ j, primeHarmonicMass (P j) ≤ A)
    (hw : ∀ w q, 0 ≤ weight w q) (hpad : ∀ w, (∑ q, weight w q) ≤ K)
    (hsingle : ∀ a ∈ F, columnSingletonCount a.1 ≤ 2 * S)
    (hcover : ∀ a ∈ F, ∃ c, ∀ j i l, decode c j i l = decide (a.1 j i = a.1 j l)) :
    (∑ a ∈ F, columnReciprocalWeight a.1 * weight a.1 a.2) ≤
      (Fintype.card Code : ℝ) * K * A ^ (J * k + S) :=
…

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