TensorWardCorrectionBound.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds on the complete finite Gaussian Ward correction after spectral coordinate contraction. Constants do not depend on the leaf cutoff.

lemma OAI.InvariantIsing.gibbsPairAverage_const_mul line 17
lemma OAI.InvariantIsing.gibbsTripleAverage_const_mul line 26
lemma OAI.InvariantIsing.abs_gibbsPairAverage_le line 37
lemma OAI.InvariantIsing.abs_gibbsTripleAverage_le line 50
def OAI.InvariantIsing.gibbsKernelCorrection line 67
Source documentation
The Gaussian correction written in terms of a contracted observable and kernel. Its three arguments retain the observable and both endpoints.
```
def gibbsKernelCorrection (w H : S → ℝ) (C : S → S → S → ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.gibbsKernelCorrection_product line 72
lemma OAI.InvariantIsing.gibbsKernelCorrection_finset_sum line 76
lemma OAI.InvariantIsing.gibbsKernelCorrection_abs_le line 91
Source documentation
Six times the contraction bound controls the entire Gaussian ratio correction, including both normalization insertions.
```
lemma gibbsKernelCorrection_abs_le {w : S → ℝ} (hw : GibbsReference w)
    (H : S → ℝ) (C : S → S → S → ℝ) {B : ℝ}
    (hC : ∀ s x y, |C s x y| ≤ B) :
    |gibbsKernelCorrection w H C| ≤ 6 * B := by
…
```
Mentions: OAI.InvariantIsing.gibbsKernelCorrection
lemma OAI.InvariantIsing.cylinderCross_add_right line 110
Distinct definitions of this name: OAI/Probability/InvariantIsing/Gaussian/CountableGaussianComparison.lean:151 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.cylinderCross_add_right@path.
def OAI.InvariantIsing.tensorRestrictionWardContraction line 115
lemma OAI.InvariantIsing.tensorRestrictionWardContraction_abs_le line 126

theorem OAI.InvariantIsing.tensorRestrictionWardCorrection_abs_le line 159

Source documentation

The complete finite Gaussian Ward correction is uniformly quadratic in the perturbation scale, independent of the leaf cutoff and all Gaussian marks. The coefficient 192 is inessential for passage to the limit.

theorem tensorRestrictionWardCorrection_abs_le {N m n : ℕ}
    (hN : 0 < N) (U : Orthogonal N) {w : S → ℝ} (hw : GibbsReference w)
    (H : S × S → ℝ) (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ)
    (treeDegree : Fin N → ℕ) (u : Fin N → ℝ) (hu : ∀ r, |u r| ≤ 2)
    (D : ℝ) (hD : 0 ≤ D) (hdegree : ∀ r, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
    (J K : Finset (Fin N)) (F : Spin N → Spin N → ℝ) (B : ℝ) (hB : 0 ≤ B)
    (hF : ∀ σ τ, |F σ τ| ≤ B) (x : S → Spin N × LabeledLeaf n) :
    |gibbsKernelCorrection (fun s : S × S => w s.1 * w s.2) H
      (tensorRestrictionWardContraction U I degree treeDegree u J K F x)| ≤
        192 * B * D * perturbationScale N ^ 2 := by
…

Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.gibbsKernelCorrection, OAI.InvariantIsing.tensorRestrictionWardContraction

lemma OAI.InvariantIsing.tensorRestrictionWardContraction_eq line 175
lemma OAI.InvariantIsing.tensorRestrictionWardCorrection_eq line 225

theorem OAI.InvariantIsing.tensorRestriction_actualWardCorrection_abs_le line 250

Source documentation

The normalized Gaussian error in the actual finite-prior Ward equation has a uniform bound tending to zero with the perturbation scale.

theorem tensorRestriction_actualWardCorrection_abs_le {N m n : ℕ} (hN : 0 < N)
    (U : SpecialOrthogonal N) {w : S → ℝ} (hw : GibbsReference w) (H : S × S → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (treeDegree : Fin N → ℕ)
    (u : Fin N → ℝ) (hu : ∀ r, |u r| ≤ 2) (D : ℝ) (hD : 0 ≤ D)
    (hdegree : ∀ r, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
    (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (J K : Finset (Fin N)) (F : Spin N → Spin N → ℝ) (B : ℝ) (hB : 0 ≤ B)
    (hF : ∀ σ τ, |F σ τ| ≤ B) (x : S → Spin N × LabeledLeaf n) :
    |(N : ℝ)⁻¹ ^ 2 * ∑ i ∈ J, ∑ j ∈ K,
      gaussianWardCorrection (fun p : S × S => w p.1 * w p.2) H
        (tensorRestrictionOffObservable i j F x U)
        (tensorRestrictionPairCovarianceDerivative I degree (tensorPerturbationAmplitude N u)
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.gaussianWardCorrection, OAI.InvariantIsing.tensorRestrictionOffObservable, OAI.InvariantIsing.tensorRestrictionPairCovarianceDerivative, OAI.InvariantIsing.tensorPerturbationAmplitude