Documentation

Lean 4 Proof

theorem gibbs_vri_with_temperature {σ_sq χ T : ℝ}
    (hT : 0 < T)
    (hvar : σ_sq = T * χ) :
    χ = σ_sq / T := by
  field_simp; linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:191

Module Section

### The Variance-Response Identity

In the same file