boltzmannDistribution
def
The Boltzmann (Gibbs) distribution on a finite configuration space Ω with Hamiltonian H : Ω → ℝ at inverse temperature β assigns to each configuration ω the probability exp(-β * H(ω)) / Z(β), where Z(β) is the canonical partition function.
Statement
noncomputable def boltzmannDistribution {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) (ω : Ω) : ℝ
- Source
- Friedli & Velenik, Statistical Mechanics of Lattice Systems (2017), Section 1.2, Eq. (1.7)
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Built on 1
- canonicalPartitionFunctionThe canonical partition function Z(β) of a system with finite configuration space Ω and Hamiltonian H : Ω → ℝ at inverse temperature β is…
Read back from the Lean
Given a finite type Ω, a function H : Ω → ℝ, a real number β, and an element ω : Ω, boltzmannDistribution H β ω is defined as Real.exp (-β * H ω) / canonicalPartitionFunction H β.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The Boltzmann (Gibbs) distribution associated with a Hamiltonian H at inverse temperature beta. -/ noncomputable def boltzmannDistribution {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) (ω : Ω) : ℝ := Real.exp (-β * H ω) / canonicalPartitionFunction H β