Documentation

Lean 4 Proof

theorem gibbsZ_pos [NeZero J] (ε x : Fin J → ℝ) (T h : ℝ) :
    0 < gibbsZ ε x T h :=
  Finset.sum_pos (fun j _ => gibbsWeight_pos ε x T h j) Finset.univ_nonempty

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:66

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file