Physlib

Physlib.StatisticalMechanics.CanonicalEnsemble.Finite

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: 1. The type of microstates `ι` is a `Fintype`. 2. The measure `μ` on `ι` is the standard counting measure. 3. The number of degrees of freedom `dof` is 0. 4. 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.

Fluctuations in Finite Systems

β-parameterization for finite systems

Derivatives of Z and numerator

Quotient rule: dU/db = U^2 - ⟨E^2⟩_β

37 declarations

instance

Finiteness of Canonical Ensembles is Preserved under Addition

Let C\mathcal{C} and C1\mathcal{C}_1 be canonical ensembles. If both C\mathcal{C} and C1\mathcal{C}_1 satisfy the finiteness condition `IsFinite` (which implies that their respective spaces of microstates are finite and their associated measures are counting measures), then their additive composition C+C1\mathcal{C} + \mathcal{C}_1 also satisfies the `IsFinite` condition.

instance

Finiteness of Canonical Ensembles is Preserved under Measurable Equivalence

Let C\mathcal{C} be a canonical ensemble. If C\mathcal{C} satisfies the finiteness condition `IsFinite` (which implies that its microstate space ι\iota is a finite type and its associated measure is the counting measure), then for any measurable equivalence e:ι1mιe : \iota_1 \simeq^m \iota, the ensemble congr(C,e)\text{congr}(\mathcal{C}, e) (the ensemble C\mathcal{C} re-indexed over the state space ι1\iota_1 via ee) also satisfies the `IsFinite` condition.

instance

Finiteness of Canonical Ensembles is Preserved under Scalar Multiplication by a Natural Number

Let C\mathcal{C} be a canonical ensemble. If C\mathcal{C} satisfies the finiteness condition `IsFinite` (which implies that its microstate space is finite and its associated measure is the counting measure), then for any natural number nNn \in \mathbb{N}, the nn-fold composition of the ensemble nCn \cdot \mathcal{C} (denoted by `nsmul n 𝓒`) also satisfies the `IsFinite` condition.

instance

A finite canonical ensemble has a finite measure

In a canonical ensemble C\mathcal{C} that satisfies the finiteness condition `IsFinite` (which implies the microstate space is finite and the measure μ\mu is the counting measure), the associated measure μ\mu is a finite measure.

instance

Non-emptiness of ι\iota implies μ0\mu \neq 0 for finite canonical ensembles

In a canonical ensemble C\mathcal{C} where the microstate space ι\iota is finite and the measure μ\mu is the counting measure (as specified by the `IsFinite` condition), if ι\iota is non-empty, then the measure μ\mu is non-zero (μ0\mu \neq 0).

definition

Shannon entropy S=kBpilnpiS = -k_B \sum p_i \ln p_i

For a canonical ensemble C\mathcal{C} with a finite set of microstates, the Shannon entropy at a given temperature TT is defined by the formula S=kBipilnpi S = -k_B \sum_{i} p_i \ln p_i where kBk_B is the Boltzmann constant and pip_i is the probability of the system being in microstate ii at temperature TT.

theorem

Mathematical Partition Function as a Finite Sum of Boltzmann Factors

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota, the mathematical partition function at temperature TT is equal to the sum of the Boltzmann factors over all microstates: Z(T)=iιeβEi Z(T) = \sum_{i \in \iota} e^{-\beta E_i} where EiE_i is the energy of microstate ii and β=1kBT\beta = \frac{1}{k_B T} is the inverse temperature.

theorem

Partition Function Z=ieβEiZ = \sum_i e^{-\beta E_i} for Finite Systems

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota, the partition function Z(T)Z(T) at temperature TT is given by the sum of the Boltzmann factors over all microstates: Z(T)=iιeβEi Z(T) = \sum_{i \in \iota} e^{-\beta E_i} where EiE_i is the energy of microstate ii and β=1kBT\beta = \frac{1}{k_B T} is the inverse temperature.

theorem

The unnormalized Boltzmann measure of a microstate is eβEie^{-\beta E_i} in a finite system

For a finite canonical ensemble C\mathcal{C} at temperature TT, the unnormalized Boltzmann measure of a microstate ii is given by exp(βEi)\exp(-\beta E_i), where β=1kBT\beta = \frac{1}{k_B T} is the inverse temperature and EiE_i is the energy associated with the state ii.

instance

The Boltzmann Measure of a Finite Canonical Ensemble is Finite

Consider a canonical ensemble C\mathcal{C} with a finite number of microstates. For any temperature TT, the Boltzmann measure μBolt(T)\mu_{\text{Bolt}}(T) (the measure where the weight of a state ii is given by eβEie^{-\beta E_i}, with β=1kBT\beta = \frac{1}{k_B T}) is a finite measure.

theorem

The probability measure of a microstate {i}\{i\} equals pip_i in finite systems

For a finite canonical ensemble C\mathcal{C} at temperature TT, the value of the normalized probability measure μProd(T)\mu_{\text{Prod}}(T) for a single microstate iιi \in \iota is equal to the probability pi(T)p_i(T) of the system being in that state.

theorem

Mean energy formula E=Eipi\langle E \rangle = \sum E_i p_i for finite canonical ensembles

For a canonical ensemble C\mathcal{C} with a finite number of microstates at temperature TT, the mean energy E(T)\langle E \rangle(T) is equal to the sum over all microstates ii of the energy EiE_i of the microstate multiplied by its probability pi(T)p_i(T) of occurrence: E(T)=iEipi(T) \langle E \rangle(T) = \sum_{i} E_i p_i(T)

theorem

Shannon entropy S=kBpilnpiS = -k_B \sum p_i \ln p_i for finite canonical ensembles

For a canonical ensemble C\mathcal{C} with a finite set of microstates at temperature TT, the Shannon entropy S(T)S(T) is given by S(T)=kBipilnpi S(T) = -k_B \sum_{i} p_i \ln p_i where kBk_B is the Boltzmann constant and pip_i is the probability of the system being in microstate ii at temperature TT.

theorem

The probability of a microstate in a finite canonical ensemble is at most 1 (pi1p_i \leq 1)

For a canonical ensemble C\mathcal{C} with a finite and non-empty set of microstates ι\iota, the probability pip_i of the system being in microstate iιi \in \iota at temperature TT is less than or equal to 1.

theorem

Strict Positivity of the Mathematical Partition Function Zmath>0Z_{\text{math}} > 0 for Finite Ensembles

For a canonical ensemble C\mathcal{C} where the set of microstates ι\iota is finite and non-empty, the mathematical partition function Zmath(T)Z_{\text{math}}(T) is strictly positive for any temperature TT. That is, Zmath(T)>0. Z_{\text{math}}(T) > 0. The mathematical partition function Zmath(T)Z_{\text{math}}(T) corresponds to the integral of the Boltzmann factor eβEe^{-\beta E} over the microstate space, which reduces to the sum iιeβEi\sum_{i \in \iota} e^{-\beta E_i} in the finite case.

theorem

Strict Positivity of the Partition Function Z>0Z > 0 for Finite Ensembles

For a canonical ensemble C\mathcal{C} where the set of microstates ι\iota is finite and non-empty, the physical partition function Z(T)Z(T) is strictly positive for any temperature TT. That is, Z(T)>0. Z(T) > 0. In this finite discrete case, the partition function Z(T)Z(T) reduces to the sum of Boltzmann factors iιeβEi\sum_{i \in \iota} e^{-\beta E_i}, where β=(kBT)1\beta = (k_B T)^{-1}. Since each exponential term is positive and the set of microstates is non-empty, the sum is strictly positive.

theorem

P(i;T)0P(i; T) \ge 0 for Finite Canonical Ensembles

For a canonical ensemble C\mathcal{C} where the set of microstates ι\iota is finite and non-empty, the probability P(i;T)P(i; T) of the system being in a microstate iιi \in \iota at temperature TT is non-negative. That is, P(i;T)0. P(i; T) \ge 0. In this finite context, the probability is given by the Boltzmann distribution P(i;T)=1Z(T)eβEiP(i; T) = \frac{1}{Z(T)} e^{-\beta E_i}, where EiE_i is the energy of the state, β=1kBT\beta = \frac{1}{k_B T} is the inverse temperature, and Z(T)Z(T) is the partition function.

theorem

The sum of probabilities in a finite canonical ensemble equals 1

For a canonical ensemble C\mathcal{C} with a finite and non-empty set of microstates ι\iota, the sum of the probabilities of all microstates iιi \in \iota at a given temperature TT is equal to 1: iιP(i;T)=1 \sum_{i \in \iota} P(i; T) = 1 where P(i;T)P(i; T) denotes the probability of the system being in microstate ii at temperature TT.

theorem

Shannon Entropy is Non-negative S0S \ge 0

For a canonical ensemble C\mathcal{C} where the set of microstates ι\iota is finite and non-empty, the Shannon entropy SS at temperature TT is non-negative. That is, S0, S \ge 0, where the Shannon entropy is defined as S=kBiιpilnpiS = -k_B \sum_{i \in \iota} p_i \ln p_i, kBk_B is the Boltzmann constant, and pip_i is the probability of the system being in microstate ii.

theorem

Shannon Entropy Equals Differential Entropy in Finite Canonical Ensembles

For a finite canonical ensemble C\mathcal{C} at temperature TT with a discrete set of microstates ι\iota, the Shannon entropy SShannon(T)S_{\text{Shannon}}(T), defined by SShannon(T)=kBiιpilnpi S_{\text{Shannon}}(T) = -k_B \sum_{i \in \iota} p_i \ln p_i (where kBk_B is the Boltzmann constant and pip_i is the probability of the system being in microstate ii), is equal to the differential entropy Sdiff(T)S_{\text{diff}}(T) of the system.

theorem

Sthermo=SShannonS_{\text{thermo}} = S_{\text{Shannon}} for Finite Canonical Ensembles

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota (satisfying the `IsFinite` condition), the thermodynamic entropy Sthermo(T)S_{\text{thermo}}(T) at temperature TT is equal to the discrete Shannon entropy SShannon(T)S_{\text{Shannon}}(T): Sthermo(T)=SShannon(T) S_{\text{thermo}}(T) = S_{\text{Shannon}}(T) where the Shannon entropy is defined as SShannon(T)=kBiιpilnpiS_{\text{Shannon}}(T) = -k_B \sum_{i \in \iota} p_i \ln p_i, kBk_B is the Boltzmann constant, and pip_i is the probability of the system being in microstate ii at temperature TT. In this finite case, all semi-classical correction factors vanish because the degrees of freedom dof=0dof = 0 and the phase space unit is 11.

theorem

Mean Square Energy for Finite Systems: E2=iEi2pi\langle E^2 \rangle = \sum_i E_i^2 p_i

For a canonical ensemble C\mathcal{C} with a finite set of microstates iιi \in \iota at temperature TT, the mean square energy E2\langle E^2 \rangle is equal to the sum over all microstates of the squared energy of each state weighted by its probability: E2=iιEi2pi(T) \langle E^2 \rangle = \sum_{i \in \iota} E_i^2 p_i(T) where EiE_i is the energy of microstate ii and pi(T)p_i(T) is the probability of the system being in that state.

theorem

Energy Variance for Finite Systems: Var(E)=E2E2\text{Var}(E) = \langle E^2 \rangle - \langle E \rangle^2

For a canonical ensemble C\mathcal{C} with a finite and non-empty set of microstates iιi \in \iota at temperature TT, the energy variance Var(E)\text{Var}(E) is equal to the mean of the squared energies weighted by their probabilities minus the square of the mean energy: Var(E)=(iιEi2pi(T))E2 \text{Var}(E) = \left( \sum_{i \in \iota} E_i^2 p_i(T) \right) - \langle E \rangle^2 where EiE_i represents the energy of microstate ii, pi(T)p_i(T) is the probability of the system being in state ii at temperature TT, and E\langle E \rangle is the mean energy of the system.

definition

Partition function Z(β)=ieβEiZ(\beta) = \sum_i e^{-\beta E_i} for finite systems

For a canonical ensemble with a finite set of microstates iιi \in \iota, the partition function ZZ is defined as a function of the inverse temperature βR\beta \in \mathbb{R} by the sum: Z(β)=iιeβEi Z(\beta) = \sum_{i \in \iota} e^{-\beta E_i} where EiE_i represents the energy of microstate ii.

theorem

The partition function Z(β)Z(\beta) is strictly positive (Z(β)>0Z(\beta) > 0) for finite non-empty systems

For a finite canonical ensemble where the set of microstates ι\iota is non-empty, the partition function Z(β)=iιeβEiZ(\beta) = \sum_{i \in \iota} e^{-\beta E_i} is strictly positive for any inverse temperature parameter βR\beta \in \mathbb{R}.

definition

Boltzmann probability pi=eβEi/Z(β)p_i = e^{-\beta E_i} / Z(\beta)

For a canonical ensemble with a finite set of microstates ι\iota, the Boltzmann probability pi(β)p_i(\beta) of a microstate iιi \in \iota at inverse temperature βR\beta \in \mathbb{R} is defined as the ratio: pi(β)=eβEiZ(β) p_i(\beta) = \frac{e^{-\beta E_i}}{Z(\beta)} where EiE_i represents the energy of microstate ii and Z(β)=jιeβEjZ(\beta) = \sum_{j \in \iota} e^{-\beta E_j} is the partition function of the system.

definition

Mean energy U(β)=iιEipi(β)U(\beta) = \sum_{i \in \iota} E_i p_i(\beta) in a finite canonical ensemble

For a canonical ensemble with a finite set of microstates ι\iota, the mean energy U(β)U(\beta) as a function of the inverse temperature parameter βR\beta \in \mathbb{R} is defined as the expected value of the energy over all microstates: U(β)=iιEipi(β) U(\beta) = \sum_{i \in \iota} E_i p_i(\beta) where EiE_i is the energy of microstate ii, and pi(β)p_i(\beta) is the Boltzmann probability of microstate ii, given by: pi(β)=eβEiZ(β) p_i(\beta) = \frac{e^{-\beta E_i}}{Z(\beta)} where Z(β)=jιeβEjZ(\beta) = \sum_{j \in \iota} e^{-\beta E_j} is the partition function of the system.

theorem

General Mean Energy equals Finite Sum Mean Energy Eβ=U(β)\langle E \rangle_\beta = U(\beta)

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota, the general measure-theoretic mean energy Eβ\langle E \rangle_\beta at a positive inverse temperature β>0\beta > 0 is equal to the finite sum definition of mean energy U(β)U(\beta), which is given by the expected value: U(β)=iιEipi(β) U(\beta) = \sum_{i \in \iota} E_i p_i(\beta) where EiE_i is the energy of microstate ii and pi(β)=eβEijιeβEjp_i(\beta) = \frac{e^{-\beta E_i}}{\sum_{j \in \iota} e^{-\beta E_j}} is the Boltzmann probability of that microstate.

theorem

Mean Energy U(β)U(\beta) is Differentiable for Finite Systems

For a canonical ensemble with a finite and non-empty set of microstates ι\iota, the mean energy U(β)U(\beta) is a differentiable function of the inverse temperature parameter βR\beta \in \mathbb{R}. The mean energy is defined as: U(β)=iιEipi(β) U(\beta) = \sum_{i \in \iota} E_i p_i(\beta) where EiE_i is the energy of microstate ii, and pi(β)=eβEijιeβEjp_i(\beta) = \frac{e^{-\beta E_i}}{\sum_{j \in \iota} e^{-\beta E_j}} is the Boltzmann probability of that state.

theorem

Z(β)Z(\beta) is Differentiable

For a finite canonical ensemble C\mathcal{C}, the partition function Z(β)=iιeβEiZ(\beta) = \sum_{i \in \iota} e^{-\beta E_i} is differentiable with respect to the inverse temperature parameter βR\beta \in \mathbb{R}.

definition

Numerator of the mean energy iEieβEi\sum_i E_i e^{-\beta E_i}

For a finite canonical ensemble C\mathcal{C} with microstates indexed by ii and corresponding energies EiE_i, this function maps the inverse temperature parameter βR\beta \in \mathbb{R} to the sum iEieβEi\sum_i E_i e^{-\beta E_i}. This sum represents the numerator used in the definition of the mean energy U(β)=iEieβEiZ(β)U(\beta) = \frac{\sum_i E_i e^{-\beta E_i}}{Z(\beta)}, where Z(β)Z(\beta) is the partition function.

theorem

The mean energy numerator iEieβEi\sum_i E_i e^{-\beta E_i} is differentiable

For a finite canonical ensemble C\mathcal{C} with microstates indexed by ii and corresponding energies EiE_i, the numerator of the mean energy, defined as the function f(β)=iEieβEif(\beta) = \sum_i E_i e^{-\beta E_i} for βR\beta \in \mathbb{R}, is differentiable with respect to β\beta.

theorem

ddβZ(β)=N(β)\frac{d}{d\beta} Z(\beta) = -N(\beta)

For a finite canonical ensemble with microstates indexed by ii and corresponding energies EiE_i, let Z(β)=ieβEiZ(\beta) = \sum_i e^{-\beta E_i} be the partition function and N(β)=iEieβEiN(\beta) = \sum_i E_i e^{-\beta E_i} be the mean energy numerator. For any inverse temperature βR\beta \in \mathbb{R}, the derivative of the partition function with respect to β\beta is equal to the negative of the mean energy numerator: ddβZ(β)=N(β).\frac{d}{d\beta} Z(\beta) = -N(\beta).

theorem

Derivative of the Mean Energy Numerator ddβN(β)=iEi2eβEi\frac{d}{d\beta} N(\beta) = -\sum_i E_i^2 e^{-\beta E_i}

For a finite canonical ensemble with microstates indexed by ii and corresponding energies EiE_i, let N(β)=iEieβEiN(\beta) = \sum_i E_i e^{-\beta E_i} denote the mean energy numerator. For any inverse temperature βR\beta \in \mathbb{R}, the derivative of this numerator with respect to β\beta is given by ddβN(β)=iEi2eβEi.\frac{d}{d\beta} N(\beta) = -\sum_i E_i^2 e^{-\beta E_i}.

theorem

Derivative of Mean Energy dUdβ=U2iEi2pi\frac{dU}{d\beta} = U^2 - \sum_i E_i^2 p_i

For a finite canonical ensemble with microstates indexed by iιi \in \iota and corresponding energies EiE_i, let U(β)U(\beta) be the mean energy and pi(β)p_i(\beta) be the Boltzmann probability of microstate ii at inverse temperature βR\beta \in \mathbb{R}. The derivative of the mean energy with respect to β\beta is given by the expression: ddβU(β)=U(β)2iιEi2pi(β),\frac{d}{d\beta} U(\beta) = U(\beta)^2 - \sum_{i \in \iota} E_i^2 p_i(\beta), where U(β)2U(\beta)^2 is the square of the mean energy and the sum represents the expected value of the squared energy E2β\langle E^2 \rangle_\beta.

theorem

dUdβ=Var(E)\frac{dU}{d\beta} = -\text{Var}(E) for Finite Canonical Ensembles

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota, let U(β)U(\beta) be the mean energy as a function of the inverse temperature β(0,)\beta \in (0, \infty). For any positive temperature T>0T > 0 with corresponding inverse temperature β=1kBT\beta = \frac{1}{k_B T}, the derivative of the mean energy with respect to β\beta is equal to the negative of the energy variance Var(E)\text{Var}(E) at that temperature: dUdβ=Var(E)\frac{dU}{d\beta} = -\text{Var}(E) where the energy variance is defined as Var(E)=E2E2\text{Var}(E) = \langle E^2 \rangle - \langle E \rangle^2.

theorem

Fluctuation-Dissipation Theorem for Finite Systems: CV=Var(E)kBT2C_V = \frac{\text{Var}(E)}{k_B T^2}

For a canonical ensemble C\mathcal{C} with a finite set of microstates ι\iota, let T>0T > 0 be a strictly positive temperature. The heat capacity CVC_V of the system is related to the variance of the energy fluctuations Var(E)\text{Var}(E) by the expression: CV=Var(E)kBT2C_V = \frac{\text{Var}(E)}{k_B T^2} where kBk_B is the Boltzmann constant and Var(E)=E2E2\text{Var}(E) = \langle E^2 \rangle - \langle E \rangle^2.