Documentation

Lean 4 Proof

theorem gibbsProb_sum_one [NeZero J] (ε x : Fin J → ℝ) (T h : ℝ) :
    ∑ j : Fin J, gibbsProb ε x T h j = 1 := by
  simp only [gibbsProb]
  rw [← Finset.sum_div]
  exact div_self (ne_of_gt (gibbsZ_pos ε x T h))

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:76

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file