Documentation

Lean 4 Proof

theorem gibbsVariance_nonneg [NeZero J] (ε x : Fin J → ℝ) (T h : ℝ)
    (f : Fin J → ℝ) :
    0 ≤ gibbsVariance ε x T h f := by
  unfold gibbsVariance gibbsMean gibbsProb
  exact variance_nonneg _ f (gibbsProb_sum_one ε x T h)
    (fun j => le_of_lt (gibbsProb_pos ε x T h j))

Dependency Graph

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:419

Module Section

### Kramers Escape Rate

In the same file