Documentation

Lean 4 Proof

def gibbsMean (ε x : Fin J → ℝ) (T h : ℝ) (f : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, f j * gibbsProb ε x T h j

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:49

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file