canonicalPartitionFunction
def
The canonical partition function Z(β) of a system with finite configuration space Ω and Hamiltonian H : Ω → ℝ at inverse temperature β is the sum over all configurations ω of exp(-β * H(ω)).
Statement
noncomputable def canonicalPartitionFunction {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) : ℝ
- Source
- Friedli & Velenik, Statistical Mechanics of Lattice Systems (2017), Section 1.2, Eq. (1.8)
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 1
- boltzmannDistributionThe Boltzmann (Gibbs) distribution on a finite configuration space Ω with Hamiltonian H : Ω → ℝ at inverse temperature β assigns to each…
Read back from the Lean
Given a finite type Ω, a function H : Ω → ℝ, and a real number β, canonicalPartitionFunction H β is defined as the finite sum over all ω : Ω of Real.exp (-β * 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 canonical partition function for a Hamiltonian on a finite configuration space at inverse temperature beta. -/ noncomputable def canonicalPartitionFunction {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) : ℝ := ∑ ω : Ω, Real.exp (-β * H ω)