Finite Canonical Ensemble

This file specializes the general measure-theoretic framework of the canonical ensemble to systems with a finite number of discrete microstates. This is a common and important case in statistical mechanics to study models like spin systems (e.g., the Ising model) and other systems with a discrete quantum state space.

Main Definitions and Results

The specialization is achieved through the IsFinite class, which asserts that:

The type of microstates ι is a Fintype.

The measure μ on ι is the standard counting measure.

The number of degrees of freedom dof is 0.

The phaseSpaceunit is 1.

These assumptions correspond to systems where the state space is fundamentally discrete, and no semi-classical approximation from a continuous phase space is needed. Consequently, the dimensionless physical quantities are directly equivalent to their mathematical counterparts.

The main results proved in this file are:

The abstract integral definitions for thermodynamic quantities (partition function, mean energy) are shown to reduce to the familiar finite sums found in introductory texts. For example, the partition function becomes Z = ∑ᵢ exp(-β Eᵢ).

The abstract thermodynamicEntropy, defined generally for measure-theoretic systems, is proven to be equal to the standard shannonEntropy (S = -k_B ∑ᵢ pᵢ log pᵢ). The semi-classical correction terms from the general theory vanish under the IsFinite assumptions.

The fluctuation-dissipation theorem in the form C_V = Var(E) / (k_B T²), which connects the heat capacity C_V to the variance of energy fluctuations, is formally proven for these systems.

This file also confirms that the IsFinite property is preserved under the composition of systems (addition, nsmul, and congr).

References

L. D. Landau & E. M. Lifshitz, Statistical Physics, Part 1, §31.

D. Tong, Lectures on Statistical Physics, §1.3.

A finite CanonicalEnsemble is one whose microstates form a finite type and whose measure is the counting measure. For such systems, the state space is inherently discrete and dimensionless, so we require dof = 0 and phaseSpaceUnit = 1.