TraceDesignations.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact lit-consistency reduction and centering for a designated trace word.

lemma OAI.TwoPointCorrelations.centered_occurrence_expansion line 15

Source documentation

Expand only the designated nonsingleton occurrences, retaining all signs.

lemma centered_occurrence_expansion [DecidableEq τ] (S : Finset τ)
    (label : τ → ι) (target : τ → A) (θ : ι → ℝ) (x : ι → A) :
    (∏ t ∈ S, ((if x (label t) = target t then (1 : ℝ) else 0) - θ (label t))) =
      ∑ U ∈ S.powerset, ((-1 : ℝ) ^ U.card * ∏ t ∈ U, θ (label t)) *
        ∏ t ∈ S \ U, if x (label t) = target t then (1 : ℝ) else 0 := by
…

lemma OAI.TwoPointCorrelations.centered_occurrence_expectation line 26

Source documentation

The signed finite expansion is integrated before taking absolute values.

lemma centered_occurrence_expectation [DecidableEq τ] (μ : FiniteLaw (ι → A))
    (S : Finset τ) (label : τ → ι) (target : τ → A) (θ : ι → ℝ)
    (F : (ι → A) → ℝ) :
    μ.average (fun x =>
      (∏ t ∈ S, ((if x (label t) = target t then (1 : ℝ) else 0) - θ (label t))) * F x) =
      ∑ U ∈ S.powerset, μ.average (fun x =>
        ((-1 : ℝ) ^ U.card * ∏ t ∈ U, θ (label t)) *
          ((∏ t ∈ S \ U, if x (label t) = target t then (1 : ℝ) else 0) * F x)) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw

lemma OAI.TwoPointCorrelations.designated_residue_zero line 44

Source documentation

A contradictory pair of lit offsets annihilates the term exactly.

lemma designated_residue_zero (μ : ι → FiniteLaw A) (S : Finset ι) (L : Finset τ)
    (label : τ → ι) (target : τ → A) (a : ι → A) (c : ℝ) (F : (ι → A) → ℝ)
    (hL : ¬LitConsistent L label target) :
    (FiniteLaw.independent μ).average (fun x => c *
      ((∏ t ∈ L, if x (label t) = target t then (1 : ℝ) else 0) *
        ((∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x))) = 0 := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.FiniteLaw.independent

theorem OAI.TwoPointCorrelations.designated_residue_bound line 55

Source documentation

This is the designated-term mixed-difference bound with literal lit occurrences, including the scalar sign and every residue-independent factor.

theorem designated_residue_bound (μ : ι → FiniteLaw A) (S : Finset ι) (L : Finset τ)
    (label : τ → ι) (target : τ → A) (a base : ι → A) (c : ℝ) (F : (ι → A) → ℝ)
    (hL : LitConsistent L label target) (hSL : Disjoint S (L.image label)) :
    |(FiniteLaw.independent μ).average (fun x => c *
      ((∏ t ∈ L, if x (label t) = target t then (1 : ℝ) else 0) *
        ((∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (μ i).weight (a i))) * F x)))| ≤
      |c| * (∏ i ∈ L.image label, (μ i).weight (litForcedTarget L label target base i)) *
        (∏ i ∈ S, (μ i).weight (a i)) *
          (FiniteLaw.independent μ).average (fun x =>
            |selectedMixedDifference S a
              (fun x => F (forceCoordinates (L.image label) (litForcedTarget L label target base) x)) x|) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.litForcedTarget, OAI.TwoPointCorrelations.selectedMixedDifference, OAI.TwoPointCorrelations.forceCoordinates