SplitBadWordSum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summing tuple and padding classes in the required order

The padding assignment is frozen before applying the nondegenerate tuple relation. It is then averaged with one reciprocal per padding class. The statement permits different symbolic words for different padding choices, since every bound is uniform in those choices.

lemma OAI.TwoPointCorrelations.sum_reciprocal_assignments line 21

lemma OAI.TwoPointCorrelations.reciprocal_product_join line 27

Source documentation

Splitting the class set preserves the original reciprocal product.

lemma reciprocal_product_join {ι : Type*} [Fintype ι] [DecidableEq ι]
    (S : Finset ι) (a : S → ℕ) (b : {i // i ∉ S} → ℕ) :
    (∏ i, ((joinCoordinates S a b i : ℕ) : ℝ)⁻¹) =
      (∏ i : S, (a i : ℝ)⁻¹) * ∏ i : {i // i ∉ S}, (b i : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.joinCoordinates

theorem OAI.TwoPointCorrelations.split_prohibited_reciprocal_bound line 39

Source documentation

The complete finite weighted estimate for one fixed equality pattern. Tuple and padding labels remain separate even after numerical enlargement.

theorem split_prohibited_reciprocal_bound {ι κ : Type*}
    [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
    {s J : ℕ} {supply : ℕ → ℕ → Prop}
    (R h : ℕ) (P Q : Finset ℕ) (word : (κ → Q) → LabeledPrimeWord ι)
    (hlen : ∀ b, (word b).word.length ≤ R)
    (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) :
    (∑ b : κ → Q, (∏ j, ((b j).val : ℝ)⁻¹) *
      ∑ a : ι → P, if ResampledProhibitedEvent (word b) h s J supply (fun i => (a i).val)
        then ∏ i, ((a i).val : ℝ)⁻¹ else 0) ≤
      (Fintype.card ι ^ 2 * (R + 1) ^ 2 : ℕ) *
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ResampledProhibitedEvent

theorem OAI.TwoPointCorrelations.split_prohibited_fiber_bound line 71

Source documentation

An actual admissible fiber may contain additional bin, distinctness, or positivity conditions. Their removal only enlarges this positive sum.

theorem split_prohibited_fiber_bound {ι κ : Type*}
    [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
    {s J : ℕ} {supply : ℕ → ℕ → Prop}
    (R h : ℕ) (P Q : Finset ℕ) (word : (κ → Q) → LabeledPrimeWord ι)
    (hlen : ∀ b, (word b).word.length ≤ R)
    (E : (ι → P) → (κ → Q) → Prop)
    (hE : ∀ a b, E a b →
      ResampledProhibitedEvent (word b) h s J supply (fun i => (a i).val))
    (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) :
    (∑ b : κ → Q, ∑ a : ι → P, if E a b then
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.ResampledProhibitedEvent, OAI.TwoPointCorrelations.primeHarmonicMass

theorem OAI.TwoPointCorrelations.CrudeWordCode.prohibited_fiber_reciprocal_bound line 104

Source documentation

Concrete application to the complete tuple/padding equality code. The input conditions concern its reconstructed numerical word; the resampling identity exchanges the order of the two weighted sums.

theorem CrudeWordCode.prohibited_fiber_reciprocal_bound {R N s J h : ℕ}
    {supply : ℕ → ℕ → Prop} (c : CrudeWordCode R N R)
    (hc : c.KindConsistent) (hi : c.RowInjective) (P Q : Finset ℕ)
    (E : (c.tupleClasses → P) → ({z : c.usedClasses // z ∉ c.tupleClasses} → Q) → Prop)
    (hE : ∀ a b, E a b →
      let w := c.numericalWord (joinCoordinates c.tupleClasses
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.joinCoordinates