ShiftTraceComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Signed expectation and comparison of the forced-word trace expansion.

def OAI.TwoPointCorrelations.shiftClosedWeight line 15
theorem OAI.TwoPointCorrelations.average_shiftMatrix_moment line 22

theorem OAI.TwoPointCorrelations.shiftMatrix_moment_comparison line 39

Source documentation

The signed expectations are compared before taking absolute values. There is one initial-site factor, and no intermediate-site factor.

theorem shiftMatrix_moment_comparison (embed : V → S) (hinj : Function.Injective embed)
    (next : E → S → S) (weight : Ω → E → S → ℝ) (weight' : Ω' → E → S → ℝ)
    (μ : FiniteLaw Ω) (ν : FiniteLaw Ω') (k : ℕ) (ε : ℝ)
    (hcompare : ∀ i u v,
      |μ.average (fun ω => shiftClosedWeight embed next (weight ω) k i u v) -
        ν.average (fun ω => shiftClosedWeight embed next (weight' ω) k i u v)| ≤ ε) :
    |μ.average (fun ω => matrixFrobeniusSq (shiftMatrix embed next (weight ω) ^ k)) -
      ν.average (fun ω => matrixFrobeniusSq (shiftMatrix embed next (weight' ω) ^ k))| ≤
      (Fintype.card V : ℝ) * (Fintype.card E : ℝ) ^ (2 * k) * ε := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.shiftClosedWeight, OAI.TwoPointCorrelations.matrixFrobeniusSq, OAI.TwoPointCorrelations.shiftMatrix