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 constant h);

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 density

helmholtzFreeEnergy : 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) measure withDensity exp(-β E)

μProd T : normalized probability measure (rescaled μBolt T)

probability T i : the density exp(-β 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 same phaseSpaceUnit is reused.

Multiplicity nsmul n 𝓒: n distinguishable, non–interacting copies (product of n 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 the Temperature 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).

https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf

https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf

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.

The energy of associated with a microstate of the canonical ensemble.

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 typically 0 as the state space is already discrete.

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 to 1.

Assumption that the phase space unit is positive.

The measure on the indexing set of microstates.

The canonical ensemble with no microstates.

The microstates of a canonical ensemble.

Properties of physical parameters

The measure

The energy of the microstates

Induction for nsmul

Non zero nature of the measure

The Boltzmann measure