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.

class CanonicalEnsemble.IsFinite {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Fintype ι] : Prop

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.

• μ_eq_count : 𝓒.μ = MeasureTheory.Measure.count
• dof_eq_zero : 𝓒.dof = 0
• phase_space_unit_eq_one : 𝓒.phaseSpaceunit = 1

instance CanonicalEnsemble.instIsFiniteProdHAdd {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) {ι1 : Type} [Fintype ι1] [MeasurableSpace ι1] [MeasurableSingletonClass ι1] (𝓒1 : CanonicalEnsemble ι1) [𝓒.IsFinite] [𝓒1.IsFinite] : (𝓒 + 𝓒1).IsFinite

instance CanonicalEnsemble.instIsFiniteCongr {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) {ι1 : Type} [Fintype ι1] [MeasurableSpace ι1] [𝓒.IsFinite] (e : ι1 ≃ᵐ ι) : (𝓒.congr e).IsFinite

instance CanonicalEnsemble.instIsFiniteForallFinNsmul {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] (n : ℕ) : (nsmul n 𝓒).IsFinite

instance CanonicalEnsemble.instIsFiniteMeasureμOfIsFinite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] : MeasureTheory.IsFiniteMeasure 𝓒.μ

instance CanonicalEnsemble.instNeZeroMeasureμOfIsFiniteOfNonempty {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] [Nonempty ι] : NeZero 𝓒.μ

In the finite (counting) case a nonempty index type gives a nonzero measure.

noncomputable def CanonicalEnsemble.shannonEntropy {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) : ℝ

The Shannon entropy of a finite canonical ensemble. This is defined by the formula S = -k_B ∑ pᵢ log pᵢ. It is proven to be equivalent to the differentialEntropy and the thermodynamicEntropy for systems satisfying the IsFinite property.

Equations

• 𝓒.shannonEntropy T = -Constants.kB * ∑ i : ι, 𝓒.probability T i * Real.log (𝓒.probability T i)

theorem CanonicalEnsemble.mathematicalPartitionFunction_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] (T : Temperature) : 𝓒.mathematicalPartitionFunction T = ∑ i : ι, Real.exp (-↑T.β * 𝓒.energy i)

theorem CanonicalEnsemble.partitionFunction_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] (T : Temperature) : 𝓒.partitionFunction T = ∑ i : ι, Real.exp (-↑T.β * 𝓒.energy i)

@[simp]

theorem CanonicalEnsemble.μBolt_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [𝓒.IsFinite] (i : ι) : (𝓒.μBolt T).real {i} = Real.exp (-↑T.β * 𝓒.energy i)

instance CanonicalEnsemble.instIsFiniteMeasureμBoltOfIsFinite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) {T : Temperature} [𝓒.IsFinite] : MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)

@[simp]

theorem CanonicalEnsemble.μProd_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [𝓒.IsFinite] (i : ι) : (𝓒.μProd T).real {i} = 𝓒.probability T i

theorem CanonicalEnsemble.meanEnergy_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) [𝓒.IsFinite] (T : Temperature) : 𝓒.meanEnergy T = ∑ i : ι, 𝓒.energy i * 𝓒.probability T i

theorem CanonicalEnsemble.entropy_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) : 𝓒.shannonEntropy T = -Constants.kB * ∑ i : ι, 𝓒.probability T i * Real.log (𝓒.probability T i)

theorem CanonicalEnsemble.probability_le_one {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) (i : ι) : 𝓒.probability T i ≤ 1

theorem CanonicalEnsemble.mathematicalPartitionFunction_pos_finite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) : 0 < 𝓒.mathematicalPartitionFunction T

Finite specialization: strict positivity of the mathematical partition function.

theorem CanonicalEnsemble.partitionFunction_pos_finite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) : 0 < 𝓒.partitionFunction T

Finite specialization: strict positivity of the (physical) partition function.

theorem CanonicalEnsemble.probability_nonneg_finite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) (i : ι) : 0 ≤ 𝓒.probability T i

Finite specialization: non-negativity (indeed positivity) of probabilities.

theorem CanonicalEnsemble.sum_probability_eq_one {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) : ∑ i : ι, 𝓒.probability T i = 1

The sum of probabilities over all microstates is 1.

theorem CanonicalEnsemble.entropy_nonneg {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) : 0 ≤ 𝓒.shannonEntropy T

The entropy of a finite canonical ensemble (Shannon entropy) is non-negative.

theorem CanonicalEnsemble.shannonEntropy_eq_differentialEntropy {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) : 𝓒.shannonEntropy T = 𝓒.differentialEntropy T

theorem CanonicalEnsemble.thermodynamicEntropy_eq_shannonEntropy {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) : 𝓒.thermodynamicEntropy T = 𝓒.shannonEntropy T

In the finite, nonempty case the thermodynamic and Shannon entropies coincide. All semi-classical correction factors vanish (dof = 0, phaseSpaceUnit = 1), so the absolute thermodynamic entropy reduces to the discrete Shannon form.

Fluctuations in Finite Systems

theorem CanonicalEnsemble.meanSquareEnergy_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) : 𝓒.meanSquareEnergy T = ∑ i : ι, 𝓒.energy i ^ 2 * 𝓒.probability T i

theorem CanonicalEnsemble.energyVariance_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] [Nonempty ι] (T : Temperature) : 𝓒.energyVariance T = ∑ i : ι, 𝓒.energy i ^ 2 * 𝓒.probability T i - 𝓒.meanEnergy T ^ 2

β-parameterization for finite systems

noncomputable def CanonicalEnsemble.mathematicalPartitionFunctionBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) : ℝ

The finite-sum partition function as a real function of the inverse temperature b = β, defined by Z(b) = ∑ i exp (-b * 𝓒.energy i).

Equations

• 𝓒.mathematicalPartitionFunctionBetaReal b = ∑ i : ι, Real.exp (-b * 𝓒.energy i)

theorem CanonicalEnsemble.mathematicalPartitionFunctionBetaReal_pos {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Nonempty ι] (b : ℝ) : 0 < 𝓒.mathematicalPartitionFunctionBetaReal b

noncomputable def CanonicalEnsemble.probabilityBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) (i : ι) : ℝ

For inverse temperature b = β, the (real-valued) Boltzmann probability of microstate i, given by exp (-b * E i) / Z(b) where Z(b) = ∑ i exp (-b * E i).

Equations

• 𝓒.probabilityBetaReal b i = Real.exp (-b * 𝓒.energy i) / 𝓒.mathematicalPartitionFunctionBetaReal b

noncomputable def CanonicalEnsemble.meanEnergyBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) : ℝ

The mean energy as a function of inverse temperature b = β in the finite case, defined by U(b) = ∑ i, E i * p_b i with p_b i = exp (-b * E i) / Z(b) and Z(b) = ∑ i, exp (-b * E i).

Equations

• 𝓒.meanEnergyBetaReal b = ∑ i : ι, 𝓒.energy i * 𝓒.probabilityBetaReal b i

theorem CanonicalEnsemble.meanEnergy_Beta_eq_finite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [MeasurableSingletonClass ι] [𝓒.IsFinite] (b : ℝ) (hb : 0 < b) : 𝓒.meanEnergyBeta b = 𝓒.meanEnergyBetaReal b

theorem CanonicalEnsemble.differentiable_meanEnergyBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Nonempty ι] : Differentiable ℝ 𝓒.meanEnergyBetaReal

Derivatives of Z and numerator

theorem CanonicalEnsemble.differentiable_mathematicalPartitionFunctionBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) : Differentiable ℝ 𝓒.mathematicalPartitionFunctionBetaReal

noncomputable def CanonicalEnsemble.meanEnergyNumerator {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) : ℝ

The numerator in the finite-sum expression of the mean energy as a function of the inverse temperature b = β, namely ∑ i, E i * exp (-b * E i) (so that U(b) = meanEnergyNumerator b / Z(b)).

Equations

• 𝓒.meanEnergyNumerator b = ∑ i : ι, 𝓒.energy i * Real.exp (-b * 𝓒.energy i)

theorem CanonicalEnsemble.differentiable_meanEnergyNumerator {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) : Differentiable ℝ 𝓒.meanEnergyNumerator

theorem CanonicalEnsemble.deriv_mathematicalPartitionFunctionBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) : deriv 𝓒.mathematicalPartitionFunctionBetaReal b = -𝓒.meanEnergyNumerator b

theorem CanonicalEnsemble.deriv_meanEnergyNumerator {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (b : ℝ) : deriv 𝓒.meanEnergyNumerator b = -∑ i : ι, 𝓒.energy i ^ 2 * Real.exp (-b * 𝓒.energy i)

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

theorem CanonicalEnsemble.deriv_meanEnergyBetaReal {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Nonempty ι] (b : ℝ) : deriv 𝓒.meanEnergyBetaReal b = 𝓒.meanEnergyBetaReal b ^ 2 - ∑ i : ι, 𝓒.energy i ^ 2 * 𝓒.probabilityBetaReal b i

theorem CanonicalEnsemble.derivWithin_meanEnergy_Beta_eq_neg_variance {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Nonempty ι] [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) : derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β = -𝓒.energyVariance T

(∂U/∂β) = -Var(E) for finite systems.

theorem CanonicalEnsemble.fluctuation_dissipation_theorem_finite {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [Nonempty ι] [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) : 𝓒.heatCapacity T = 𝓒.energyVariance T / (Constants.kB * ↑T.val ^ 2)

FDT for finite canonical ensembles: C_V = Var(E) / (k_B T²).