Documentation

Lean 4 Proof

theorem gibbsMean_hasDerivAt [NeZero J] (ε x : Fin J → ℝ) (T : ℝ) (hT : T ≠ 0)
    (h : ℝ) (f : Fin J → ℝ) :
    HasDerivAt (fun h' => gibbsMean ε x T h' f)
      (∑ j, f j * (gibbsProb ε x T h j / T *
        (x j - gibbsMean ε x T h (fun k => x k)))) h := by
  change HasDerivAt (fun h' => ∑ j : Fin J, f j * gibbsProb ε x T h' j) _ h
  have := HasDerivAt.sum fun j (_ : j ∈ Finset.univ) =>
    HasDerivAt.const_mul (f j) (gibbsProb_hasDerivAt ε x T hT h j)
  simp only [Finset.sum_fn] at this
  exact this

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:244

Module Section

### Derivative Form of the VRI

In the same file