Documentation

Lean 4 Proof

theorem gibbs_static_vri [NeZero J] (ε x : Fin J → ℝ) (T : ℝ)
    (_hT : 0 < T) :
    let P := gibbsProb ε x T 0
    let μ := ∑ j, x j * P j
    let σ_sq := (∑ j, x j ^ 2 * P j) - μ ^ 2
    -- The VRI: σ² = T · χ, expressed as σ² = Σ P_j · x_j · (x_j - μ)
    -- (the right side equals T · χ because χ = (1/T) · Σ P_j · x_j · (x_j - μ))
    σ_sq = ∑ j, P j * x j * (x j - μ) :=
  (algebraic_vri_core (gibbsProb ε x T 0) x (gibbsProb_sum_one ε x T 0)).symm

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:179

Module Section

### The Variance-Response Identity

In the same file