Documentation

Lean 4 Proof

theorem gibbsProb_hasDerivAt [NeZero J] (ε x : Fin J → ℝ) (T : ℝ) (hT : T ≠ 0)
    (h : ℝ) (j : Fin J) :
    HasDerivAt (fun h' => gibbsProb ε x T h' j)
      (gibbsProb ε x T h j / T * (x j - gibbsMean ε x T h (fun k => x k))) h := by
  have hw := gibbsWeight_hasDerivAt ε x T hT h j
  have hZ := gibbsZ_hasDerivAt ε x T hT h
  have hZpos := gibbsZ_pos (J := J) ε x T h
  have hZne : gibbsZ ε x T h ≠ 0 := ne_of_gt hZpos
  -- Quotient rule: d/dh [w/Z] = (w'Z - wZ')/Z²
  have hd := HasDerivAt.div hw hZ hZne
  -- Show our function matches the quotient form
  have hfun : (fun h' => gibbsProb ε x T h' j) =
      (fun h' => gibbsWeight ε x T h' j) / gibbsZ ε x T := by
    ext h'; simp [gibbsProb, Pi.div_apply]
  rw [hfun]
  -- Now show derivative values match
  -- Pre-factor the sums to avoid ring failing on sums with inverses
  refine hd.congr_deriv ?_
  -- Factor x_k/T * w_k = x_k * w_k / T in the quotient rule sum
  have hsum : ∑ k : Fin J, x k / T * gibbsWeight ε x T h k =
    (∑ k : Fin J, x k * gibbsWeight ε x T h k) / T := by
    rw [Finset.sum_div]; congr 1; ext k; ring
  rw [hsum]
  simp only [gibbsProb, gibbsMean]
  -- Factor x_k * (w_k / Z) = x_k * w_k / Z in the mean
  have hmean : ∑ k : Fin J, x k * (gibbsWeight ε x T h k / gibbsZ ε x T h) =
    (∑ k : Fin J, x k * gibbsWeight ε x T h k) / gibbsZ ε x T h := by
    rw [Finset.sum_div]; congr 1; ext k; ring
  rw [hmean]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:212

Module Section

### Derivative Form of the VRI

In the same file