Documentation

Lean 4 Proof

theorem gibbs_susceptibility_vri [NeZero J] (ε x : Fin J → ℝ) (T : ℝ) (hT : T ≠ 0)
    (h₀ : ℝ) :
    HasDerivAt (fun h => gibbsMean ε x T h (fun j => x j))
      ((1 / T) * gibbsVariance ε x T h₀ (fun j => x j)) h₀ := by
  have hd := gibbsMean_hasDerivAt ε x T hT h₀ (fun j => x j)
  refine hd.congr_deriv ?_
  rw [gibbsMean_deriv_eq_covariance ε x T hT]
  congr 1
  -- Need: E[x·x] - E[x]·E[x] = E[x²] - E[x]²
  unfold gibbsVariance gibbsMean
  congr 1
  · congr 1; ext j; ring
  · ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:277

Module Section

### Derivative Form of the VRI

In the same file