Documentation

Lean 4 Proof

def gibbsVariance (ε x : Fin J → ℝ) (T h : ℝ) (f : Fin J → ℝ) : ℝ :=
  gibbsMean ε x T h (fun j => f j ^ 2) - (gibbsMean ε x T h f) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/GibbsMeasure.lean:53

Module Section

Gibbs Measure for Finite Discrete Systems:

In the same file