EncodedBadSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The prohibited-word reciprocal estimate summed over all finite codes.

theorem OAI.TwoPointCorrelations.encoded_prohibited_sum_le line 13

theorem OAI.TwoPointCorrelations.bounded_encoded_prohibited_sum_le line 81

Source documentation

Length and slot-count summation retain the one-prime saving.

theorem bounded_encoded_prohibited_sum_le (T h s J : ℕ) (P Q : Finset ℕ)
    (supply : ℕ → ℕ → Prop)
    (hP : ∀ p ∈ P, p.Prime) (hVP : 1 ≤ primeHarmonicMass P)
    (H B : ℕ) (hH : 0 < H) (hB : 1 ≤ B)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ B) :
    (∑ R : Fin (s + 1), ∑ e : PrimeWordEncoding R.val T P Q,
      if e.Prohibited h s J supply then e.weight else 0) ≤
      badCatalogCost s T (primeHarmonicMass P) (primeHarmonicMass Q) *
        ((H : ℝ)⁻¹ + (1 + Real.log B) / H) := by
…

Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.PrimeWordEncoding, OAI.TwoPointCorrelations.badCatalogCost