Ward.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-volume Gibbs rotation identity

Differentiation of a normalized Gibbs average produces the observable variation and its covariance with the Hamiltonian variation. Haar invariance then gives their exact integral identity. The spin prior may have zero weights. No limiting Ward equations or pressure bounds are assumed here.

def OAI.InvariantIsing.gibbsAverage line 25
Source documentation
Finite normalized Gibbs expectation, for an arbitrary nonzero positive prior.
```
def gibbsAverage (w H A : S → ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.abs_gibbsAverage_le line 28
lemma OAI.InvariantIsing.measurable_gibbsAverage line 32

lemma OAI.InvariantIsing.hasDerivAt_gibbsAverage line 44

Source documentation

Derivative of a finite Gibbs expectation: the variation of the observable plus its Gibbs covariance with the variation of the Hamiltonian.

lemma hasDerivAt_gibbsAverage {w : S → ℝ} (hw : GibbsReference w)
    {H A : ℝ → S → ℝ} {dH dA : S → ℝ} {t : ℝ}
    (hH : ∀ σ, HasDerivAt (fun s => H s σ) (dH σ) t)
    (hA : ∀ σ, HasDerivAt (fun s => A s σ) (dA σ) t) :
    HasDerivAt (fun s => gibbsAverage w (H s) (A s))
      (gibbsAverage w (H t) dA +
        gibbsAverage w (H t) (fun σ => A t σ * dH σ) -
        gibbsAverage w (H t) (A t) * gibbsAverage w (H t) dH) t := by
…

Mentions: OAI.InvariantIsing.gibbsAverage

lemma OAI.InvariantIsing.abs_gibbsVariation_le line 62

theorem OAI.InvariantIsing.integral_gibbs_rotation_identity line 86

Source documentation

Exact finite-volume Haar Ward identity. All regularity assumptions concern finite-dimensional derivatives; none assumes a limiting overlap identity.

theorem integral_gibbs_rotation_identity {N : ℕ}
    (μ : Measure (Orthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    (R : ℝ → Orthogonal N) (hR : R 0 = 1)
    {w : S → ℝ} (hw : GibbsReference w)
    (H A : Orthogonal N → S → ℝ)
    (hHm : ∀ σ, Measurable (fun U => H U σ))
    (hAm : ∀ σ, Measurable (fun U => A U σ))
    (dH dA : ℝ → Orthogonal N → S → ℝ)
    (hdHm : ∀ σ, Measurable (fun U => dH 0 U σ))
    (hdAm : ∀ σ, Measurable (fun U => dA 0 U σ))
    (hHd : ∀ U t, t ∈ Set.Ioo (-1 : ℝ) 1 → ∀ σ,
      HasDerivAt (fun s => H (R s * U) σ) (dH t U σ) t)
…

Mentions: OAI.InvariantIsing.Orthogonal