OAI/Probability/InvariantIsing/Arrays/TensorDiagonalWardCorrectionBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorRestrictionDiagonalWardContraction line 18
2. lemma OAI.InvariantIsing.tensorRestrictionDiagonalWardContraction_eq line 23
3. lemma OAI.InvariantIsing.tensorRestrictionDiagonalWardCorrection_eq line 35
4. theorem OAI.InvariantIsing.tensorRestriction_actualDiagonalWardCorrection_abs_le line 58

   Source documentation

   The exact one-replica Gaussian correction, with its single covariance kernel rather than a doubled Hamiltonian coefficient.

   theorem tensorRestriction_actualDiagonalWardCorrection_abs_le [Fintype S] {N m n : ℕ}
       (hN : 0 < N) (U : SpecialOrthogonal N) {w : S → ℝ} (hw : GibbsReference w) (H : 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)) (x : S → Spin N × LabeledLeaf n) :
       |(N : ℝ)⁻¹ ^ 2 * ∑ i ∈ J, ∑ j ∈ K,
         gaussianWardCorrection w H (tensorRestrictionDiagonalObservable i j x U)
           (tensorRestrictionCovarianceDerivative I degree (tensorPerturbationAmplitude N u)
             (fun a => tensorPathProfile I degree n treeDegree h a) x i j U)| ≤
         48 * D * perturbationScale N ^ 2 := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.gaussianWardCorrection, OAI.InvariantIsing.tensorRestrictionDiagonalObservable, OAI.InvariantIsing.tensorRestrictionCovarianceDerivative, OAI.InvariantIsing.tensorPerturbationAmplitude, OAI.InvariantIsing.tensorPathProfile