Canonical Ensemble: Core Definitions #
A canonical ensemble describes a system in thermal equilibrium with a heat bath at fixed
temperature T
. This file gives a measure–theoretic, semi–classical formalization intended to
work uniformly for discrete (counting measure) and continuous (Lebesgue–type) models.
1. Semi–Classical Normalization #
Classical phase–space integrals produce dimensionful quantities. To obtain dimensionless thermodynamic objects (and an absolute entropy) we introduce:
phaseSpaceUnit : ℝ
(physically Planck's constanth
);dof : ℕ
the number of degrees of freedom.
The physical partition function is obtained from the mathematical one by dividing by
phaseSpaceUnit ^ dof
. This yields the standard semi–classical correction preventing
ambiguities such as the Gibbs paradox.
2. Mathematical vs Physical Quantities #
We keep both layers:
Mathematical / raw:
mathematicalPartitionFunction (T)
: ∫ exp(-β E) dμprobability
(density w.r.t.μ
)differentialEntropy
(can be negative, unit–dependent)
Physical / dimensionless:
partitionFunction
:Z = Z_math / h^dof
physicalProbability
: dimensionless densityhelmholtzFreeEnergy
:F = -kB T log Z
thermodynamicEntropy
: absolute entropy(U - F)/T = -kB ∫ ρ_phys log ρ_phys
Each physical quantity is expressed explicitly in terms of its mathematical ancestor.
3. Core Structure #
We assume phaseSpaceUnit > 0
and μ
σ–finite. No probability assumption is imposed:
normalization is recovered via the Boltzmann weighted measure.
4. Boltzmann & Probability Measures #
μBolt T
: Boltzmann (unnormalized) measurewithDensity exp(-β E)
μProd T
: normalized probability measure (rescaledμBolt T
)probability T i
: the densityexp(-β E(i)) / Z_math
physicalProbability
:probability * (phase_space_unit ^ dof)
5. Energies & Entropies #
meanEnergy
: expectation of energy underμProd
.differentialEntropy
:-kB ∫ log(probability) dμProd
thermodynamicEntropy
:-kB ∫ log(physicalProbability) dμProd
(proved later to coincide with the textbook(U - F)/T
).
A helper lemma supplies positivity of the partition function under mild assumptions and
non–negativity criteria for the entropy when probability ≤ 1
(automatic in finite discrete
settings, not in general continuous ones).
6. Algebraic Operations #
We construct composite ensembles:
- Addition
(𝓒₁ + 𝓒₂)
on product microstates: energies add, measures take product, degrees of freedom add, and (physically) the samephaseSpaceUnit
is reused. - Multiplicity
nsmul n 𝓒
:n
distinguishable, non–interacting copies (product ofn
copies). - Transport along measurable equivalences via
congr
.
These operations respect partition functions, free energies, and (under suitable hypotheses) mean energies and integrability.
7. Notational & Implementation Notes #
- We work over an arbitrary measurable type
ι
, allowing both finite and continuous models. β
is accessed through theTemperature
structure (T.β
).- Most positivity / finiteness conditions are hypotheses on lemmas instead of global axioms, enabling reuse in formal derivations of fluctuation and response identities.
8. References #
- L. D. Landau & E. M. Lifshitz, Statistical Physics, Part 1.
- D. Tong, Cambridge Lecture Notes (sections on canonical ensemble).
9. Roadmap #
Subsequent files (Lemmas.lean
) prove:
- Relations among entropies and free energies.
- Fundamental identity
F = U - T S
. - Derivative (response) formulas:
U = -∂_β log Z
.
A Canonical ensemble is described by a type ι
, corresponding to the type of microstates,
and a map ι → ℝ
which associates which each microstate an energy
and physical constants needed to define dimensionless thermodynamic quantities.
- energy : ι → ℝ
The energy of associated with a mircrostate of the canonical ensemble.
- dof : ℕ
The number of degrees of freedom, used to make the partition function dimensionless. For a classical system of N particles in 3D, this is
3N
. For a system of N spins, this is typically0
as the state space is already discrete. - phaseSpaceunit : ℝ
The unit of action used to make the phase space volume dimensionless. This constant is necessary to define an absolute (rather than relative) thermodynamic entropy. In the semi-classical approach, this unit is identified with Planck's constant
h
. For discrete systems with a counting measure, this unit should be set to1
. Assumption that the phase space unit is positive.
- energy_measurable : Measurable self.energy
- μ : MeasureTheory.Measure ι
The measure on the indexing set of microstates.
- μ_sigmaFinite : MeasureTheory.SigmaFinite self.μ
Instances For
The addition of two CanonicalEnsemble
. The degrees of freedom are added.
Note: This is only physically meaningful if the two systems share the same phase_space_unit
.
Equations
- One or more equations did not get rendered due to their size.
The canonical ensemble with no microstates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a measurable equivalence e : ι1 ≃ᵐ ι
, this is the corresponding canonical ensemble
on ι1
. The physical properties (dof
, phase_space_unit
) are unchanged.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scalar multiplication of CanonicalEnsemble
, defined such that
nsmul n 𝓒
represents n
non-interacting, distinguishable copies of the ensemble 𝓒
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The microstates of a canonical ensemble.
Equations
- 𝓒.microstates = ι
Instances For
Properties of physical parameters #
The measure #
The energy of the microstates #
Induction for nsmul #
Non zero nature of the measure #
The Boltzmann measure #
The Boltzmann measure on the space of microstates.
Equations
- 𝓒.μBolt T = 𝓒.μ.withDensity fun (i : ι) => ENNReal.ofReal (Real.exp (-↑T.β * 𝓒.energy i))
Instances For
The Mathematical Partition Function #
The mathematical partition function, defined as the integral of the Boltzmann factor.
This quantity may have physical dimensions. See CanonicalEnsemble.partitionFunction
for
the dimensionless physical version.
Equations
- 𝓒.mathematicalPartitionFunction T = (𝓒.μBolt T).real Set.univ
Instances For
The mathematicalPartitionFunction_nsmul
function of n
copies of a canonical ensemble.
The partition function is strictly positive provided the underlying measure is non-zero and the Boltzmann measure is finite.
The probability density #
The probability density function of the canonical ensemble.
Note: In the general measure-theoretic case, this is a density with respect to the
underlying measure 𝓒.μ
and is not necessarily less than or equal to 1. In the
case of a finite ensemble with the counting measure, this value corresponds to the
probability of the microstate.
Equations
- 𝓒.probability T i = Real.exp (-↑T.β * 𝓒.energy i) / 𝓒.mathematicalPartitionFunction T
Instances For
The probability measure #
The probability measure associated with the Boltzmann distribution of a canonical ensemble.
Instances For
Integrability of energy #
The mean energy #
The mean energy of the canonical ensemble at temperature T
.
Instances For
The differential entropy #
The (differential) entropy of the canonical ensemble. In the continuous case, this quantity
is not absolute but depends on the choice of units for the measure. It can be negative.
See thermodynamicEntropy
for the absolute physical quantity.
Equations
- 𝓒.differentialEntropy T = -Constants.kB * ∫ (i : ι), Real.log (𝓒.probability T i) ∂𝓒.μProd T
Instances For
Probabilities are non-negative, assuming a positive partition function.
Probabilities are strictly positive.
General entropy non-negativity under a pointwise upper bound probability ≤ 1
.
This assumption holds automatically in the finite/counting case (since sums bound each term),
but can fail in general (continuous) settings; hence we separate it as a hypothesis.
Finite case: see CanonicalEnsemble.entropy_nonneg
in Finite
.
Thermodynamic Quantities #
These are the dimensionless physical quantities derived from the mathematical definitions
by incorporating the phase space volume 𝓒.phaseSpaceUnit ^ 𝓒.dof
.
The dimensionless thermodynamic partition function, Z = Z_math / h^dof
.
Equations
- 𝓒.partitionFunction T = 𝓒.mathematicalPartitionFunction T / 𝓒.phaseSpaceunit ^ 𝓒.dof
Instances For
A rewriting form convenient under a coercion to a temperature obtained from an inverse temperature.
The logarithm of the mathematical partition function as an integral.
The Helmholtz free energy, F = -k_B T log(Z)
. This is the central
quantity from which other thermodynamic properties are derived.
Equations
- 𝓒.helmholtzFreeEnergy T = -Constants.kB * ↑T.val * Real.log (𝓒.partitionFunction T)
Instances For
The dimensionless physical probability density. This is is the probability density w.r.t. the
measure, obtained by dividing the phase space measure by the fundamental unit h^dof
, making the
probability density ρ_phys = ρ_math * h^dof
dimensionless.
Equations
- 𝓒.physicalProbability T i = 𝓒.probability T i * 𝓒.phaseSpaceunit ^ 𝓒.dof
Instances For
Normalization of the dimensionless physical probability density over the base measure.
The absolute thermodynamic entropy, defined from its statistical mechanical foundation as the Gibbs-Shannon entropy of the dimensionless physical probability distribution. This corresponds to Landau & Lifshitz, Statistical Physics, §7, Eq. 7.12.
Equations
- 𝓒.thermodynamicEntropy T = -Constants.kB * ∫ (i : ι), Real.log (𝓒.physicalProbability T i) ∂𝓒.μProd T