CenteredWordMajorant.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Apply exact uniform singleton centering to the complete signed word.

lemma OAI.TwoPointCorrelations.uniform_singleton_target_lt line 14

lemma OAI.TwoPointCorrelations.uniform_word_designation_zero line 24

Source documentation

Contradictory lit tests vanish even with all singleton factors retained.

lemma uniform_word_designation_zero (B : ℕ) (p : ι → ℕ)
    (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (label : τ → ι) (target : τ → Fin B) (base : ι → Fin B)
    (htarget : ∀ t, (target t).val < p (label t)) (U : Finset τ)
    (R : ℝ) (G : (ι → Fin B) → ℝ)
    (hL : ¬LitConsistent (nonsingletonSlots label \ U) label target) :
    (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
      (fun x => (R * ((-1 : ℝ) ^ U.card * ∏ t ∈ U, (p (label t) : ℝ)⁻¹)) *
        ((∏ t ∈ nonsingletonSlots label \ U,
          if x (label t) = target t then (1 : ℝ) else 0) *
          ((∏ i ∈ singletonLabels label,
            ((if x i = singletonTarget label target base i then (1 : ℝ) else 0) -
…

Mentions: OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.singletonTarget

theorem OAI.TwoPointCorrelations.uniform_centered_word_majorant line 56

Source documentation

Full-word majorant. Absolute values are introduced only after the signed expansion and exact singleton integrations have been performed.

theorem uniform_centered_word_majorant (B : ℕ) (p : ι → ℕ)
    (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (label : τ → ι) (target : τ → Fin B) (base : ι → Fin B)
    (htarget : ∀ t, (target t).val < p (label t))
    (R : ℝ) (hR : 0 ≤ R) (G : (ι → Fin B) → ℝ) :
    |(FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
      (fun x => R * (∏ t,
        ((if x (label t) = target t then (1 : ℝ) else 0) - (p (label t) : ℝ)⁻¹)) * G x)| ≤
      ∑ U ∈ (nonsingletonSlots label).powerset,
        if LitConsistent (nonsingletonSlots label \ U) label target then
          R * designatedReciprocal p (singletonLabels label) (nonsingletonSlots label \ U) U label *
            (FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.designatedReciprocal, OAI.TwoPointCorrelations.singletonLabels

theorem OAI.TwoPointCorrelations.uniform_centered_word_crude_bound line 89

Source documentation

The crude mixed-difference bound can be used after the signed singleton integration, retaining every exact reciprocal coefficient.

theorem uniform_centered_word_crude_bound (B : ℕ) (p : ι → ℕ)
    (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (label : τ → ι) (target : τ → Fin B) (base : ι → Fin B)
    (htarget : ∀ t, (target t).val < p (label t))
    (R : ℝ) (hR : 0 ≤ R) (G : (ι → Fin B) → ℝ) (hG : ∀ x, |G x| ≤ 1) :
    |(FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
      (fun x => R * (∏ t,
        ((if x (label t) = target t then (1 : ℝ) else 0) - (p (label t) : ℝ)⁻¹)) * G x)| ≤
      ∑ U ∈ (nonsingletonSlots label).powerset,
        R * designatedReciprocal p (singletonLabels label) (nonsingletonSlots label \ U) U label *
          2 ^ (singletonLabels label).card := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.designatedReciprocal, OAI.TwoPointCorrelations.singletonLabels