Documentation

Lean 4 Proof

theorem gibbsMean_deriv_eq_covariance [NeZero J] (ε x : Fin J → ℝ) (T : ℝ) (_hT : T ≠ 0)
    (h : ℝ) (f : Fin J → ℝ) :
    ∑ j, f j * (gibbsProb ε x T h j / T *
      (x j - gibbsMean ε x T h (fun k => x k))) =
    (1 / T) * (gibbsMean ε x T h (fun j => f j * x j) -
      gibbsMean ε x T h f * gibbsMean ε x T h (fun k => x k)) := by
  simp only [gibbsMean]
  set P := gibbsProb ε x T h
  -- Factor 1/T out of each term
  have h1 : ∀ i : Fin J, f i * (P i / T * (x i - ∑ k, x k * P k)) =
    (1 / T) * (f i * P i * (x i - ∑ k, x k * P k)) := by intro i; ring
  simp_rw [h1, ← Finset.mul_sum]
  congr 1
  -- Expand f_i * P_i * (x_i - μ) = f_i * x_i * P_i - f_i * P_i * μ
  have h2 : ∀ i : Fin J, f i * P i * (x i - ∑ k, x k * P k) =
    f i * x i * P i - f i * P i * ∑ k, x k * P k := by intro i; ring
  simp_rw [h2, Finset.sum_sub_distrib, ← Finset.sum_mul]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:256

Module Section

### Derivative Form of the VRI

In the same file