Documentation

Lean 4 Proof

theorem gibbs_vri_full [NeZero J] (ε x : Fin J → ℝ) (T : ℝ) (hT : 0 < T) (h₀ : ℝ) :
    let χ := (1 / T) * gibbsVariance ε x T h₀ (fun j => x j)
    gibbsVariance ε x T h₀ (fun j => x j) = T * χ := by
  simp only
  field_simp

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:293

Module Section

### Derivative Form of the VRI

In the same file