Documentation

Lean 4 Proof

def gibbsWeight (ε x : Fin J → ℝ) (T h : ℝ) (j : Fin J) : ℝ :=
  Real.exp ((h * x j - ε j) / T)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:37

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file