Documentation

Lean 4 Proof

theorem gibbsProb_pos [NeZero J] (ε x : Fin J → ℝ) (T h : ℝ) (j : Fin J) :
    0 < gibbsProb ε x T h j :=
  div_pos (gibbsWeight_pos ε x T h j) (gibbsZ_pos ε x T h)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:71

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file