Documentation

Lean 4 Proof

private lemma gibbsWeight_hasDerivAt (ε x : Fin J → ℝ) (T : ℝ) (_hT : T ≠ 0)
    (h : ℝ) (j : Fin J) :
    HasDerivAt (fun h' => gibbsWeight ε x T h' j)
      (x j / T * gibbsWeight ε x T h j) h := by
  unfold gibbsWeight
  have inner : HasDerivAt (fun h' => (h' * x j - ε j) / T) (x j / T) h := by
    have := ((hasDerivAt_id h).mul_const (x j)).sub_const (ε j)
    convert this.div_const T using 1; ring
  convert inner.exp using 1; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:87

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file