Documentation

Lean 4 Proof

theorem gibbsZ_hasDerivAt (ε x : Fin J → ℝ) (T : ℝ) (hT : T ≠ 0) (h : ℝ) :
    HasDerivAt (gibbsZ ε x T)
      (∑ j : Fin J, x j / T * gibbsWeight ε x T h j) h := by
  change HasDerivAt (fun h' => ∑ j : Fin J, gibbsWeight ε x T h' j)
    (∑ j : Fin J, x j / T * gibbsWeight ε x T h j) h
  have := HasDerivAt.sum fun j (_ : j ∈ Finset.univ) =>
    gibbsWeight_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:98

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file