Canonical Ensemble: Thermodynamic Identities and Relations #

This file develops relations between the mathematical objects defined in Basic.lean and the physical thermodynamic quantities, together with calculus identities for the canonical ensemble.

Contents Overview #

Helmholtz Free Energies

mathematicalHelmholtzFreeEnergy
Relation to physical helmholtzFreeEnergy with semi–classical correction.

Entropy Relations

Pointwise logarithm of (mathematical / physical) Boltzmann probabilities.
Key identity: differentialEntropy = kB * β * meanEnergy + kB * log Z_math
Fundamental link: thermodynamicEntropy = differentialEntropy - kB * dof * log h (semi–classical correction term).
Specializations removing the correction when dof = 0 or phaseSpaceUnit = 1.

Fundamental Thermodynamic Identity

Proof of F = U - T S_thermo.
Equivalent rearrangements giving entropy from energies and free energy.
Discrete / normalized specialization (no correction).

Mean energy as U = - d/dβ log Z_math and likewise with the physical partition function (constant factor cancels).

Design Notes #

All derivative statements are given as derivWithin on Set.Ioi 0, matching the physical domain β > 0.
Assumptions (finiteness, integrability) are parameterized to keep lemmas reusable.
Semi–classical correction appears systematically as kB * dof * log phaseSpaceUnit.

References #

Same references as Basic.lean (Landau–Lifshitz; Tong), especially the identities F = U - T S and U = -∂_β log Z.

source

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

ℝ

An intermediate potential defined from the mathematical partition function. See helmholtzFreeEnergy for the physical thermodynamic quantity.

Equations

𝓒.mathematicalHelmholtzFreeEnergy T = -Constants.kB * ↑T.val * Real.log (𝓒.mathematicalPartitionFunction T)

Instances For

source

theorem CanonicalEnsemble.helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] :

𝓒.helmholtzFreeEnergy T = 𝓒.mathematicalHelmholtzFreeEnergy T + Constants.kB * ↑T.val * ↑𝓒.dof * Real.log 𝓒.phaseSpaceunit

The relationship between the physical Helmholtz Free Energy and the Helmholtz Potential.

source

theorem CanonicalEnsemble.differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) :

𝓒.differentialEntropy T = Constants.kB * ↑T.β * 𝓒.meanEnergy T + Constants.kB * Real.log (𝓒.mathematicalPartitionFunction T)

General identity: S_diff = kB β ⟨E⟩ + kB log Z_math. This connects the differential entropy to the mean energy and the mathematical partition function. Integrability of log (probability …) follows from the pointwise formula.

source

theorem CanonicalEnsemble.log_probability {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (i : ι) :

Real.log (𝓒.probability T i) = -↑T.β * 𝓒.energy i - Real.log (𝓒.mathematicalPartitionFunction T)

Pointwise logarithm of the Boltzmann probability.

source

@[simp]

theorem CanonicalEnsemble.kB_mul_beta (T : Temperature) (hT : 0 < T.val) :

Constants.kB * ↑T.β = 1 / ↑T.val

Auxiliary identity: kB · β = 1 / T. β is defined as 1 / (kB · T) (see Temperature.β).

source

theorem CanonicalEnsemble.thermodynamicEntropy_eq_differentialEntropy_sub_correction {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] :

𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T - Constants.kB * ↑𝓒.dof * Real.log 𝓒.phaseSpaceunit

Fundamental relation between thermodynamic and differential entropy: S_thermo = S_diff - kB * dof * log h.

source

theorem CanonicalEnsemble.thermodynamicEntropy_eq_differentialEntropy_of_dof_zero {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) (h0 : 𝓒.dof = 0) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] :

𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T

No semiclassical correction when dof = 0.

source

theorem CanonicalEnsemble.thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) (h1 : 𝓒.phaseSpaceunit = 1) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] :

𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T

No semiclassical correction when phase_space_unit = 1.

The Fundamental Thermodynamic Identity #

source

theorem CanonicalEnsemble.helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hT : 0 < T.val) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) :

𝓒.helmholtzFreeEnergy T = 𝓒.meanEnergy T - ↑T.val * 𝓒.thermodynamicEntropy T

The Helmholtz free energy F is related to the mean energy U and the absolute thermodynamic entropy S by the identity F = U - TS. This theorem shows that the statistically-defined quantities in this framework correctly satisfy this principle of thermodynamics.

source

theorem CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hT : 0 < T.val) (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) :

𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + Constants.kB * ↑𝓒.dof * Real.log 𝓒.phaseSpaceunit

Theorem: Helmholtz identity with semi–classical correction term. Physical identity (always true for T > 0) : (U - F)/T = S_thermo and: S_thermo = S_diff - kB * dof * log h. Hence: S_diff = (U - F)/T + kB * dof * log h. This theorem gives the correct relation for the (mathematical / differential) entropy. (Removing the correction is only valid in normalized discrete cases with dof = 0 (or phaseSpaceUnit = 1).)

source

theorem CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hT : 0 < T.val) (hE : MeasureTheory.Integrable 𝓒.energy (𝓒.μProd T)) (hNorm : 𝓒.dof = 0 ∨ 𝓒.phaseSpaceunit = 1) :

𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val

Discrete / normalized specialization of the previous theorem. If either dof = 0 (no semiclassical correction) or phaseSpaceUnit = 1 (so log h = 0), the correction term vanishes and we recover the bare Helmholtz identity for the (differential) entropy.

source

theorem CanonicalEnsemble.hasDerivWithinAt_log_comp {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) :

HasDerivWithinAt (fun (t : ℝ) => Real.log (f t)) ((f x)⁻¹ * f') s x

Chain rule convenience lemma for log ∘ f on a set.

source

theorem CanonicalEnsemble.hasDerivWithinAt_log_comp' {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x : ℝ} (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0) :

HasDerivWithinAt (fun (t : ℝ) => Real.log (f t)) (1 / f x * f') s x

A version rewriting the derivative value with 1 / f x.

source

theorem CanonicalEnsemble.integral_bolt_eq_integral_mul_exp {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (φ : ι → ℝ) :

∫ (x : ι), φ x ∂𝓒.μBolt T = ∫ (x : ι), φ x * Real.exp (-↑T.β * 𝓒.energy x) ∂𝓒.μ

source

theorem CanonicalEnsemble.integral_energy_bolt {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) :

∫ (x : ι), 𝓒.energy x ∂𝓒.μBolt T = ∫ (x : ι), 𝓒.energy x * Real.exp (-↑T.β * 𝓒.energy x) ∂𝓒.μ

A specialization of integral_bolt_eq_integral_mul_exp to the energy observable.

source

theorem CanonicalEnsemble.meanEnergy_eq_ratio_of_integrals {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) :

𝓒.meanEnergy T = (∫ (i : ι), 𝓒.energy i * Real.exp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) / ∫ (i : ι), Real.exp (-↑T.β * 𝓒.energy i) ∂𝓒.μ

The mean energy can be expressed as a ratio of integrals.

source

theorem CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_mathZ_of_beta {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hT_pos : 0 < T.val) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (h_deriv : HasDerivWithinAt (fun (β : ℝ) => ∫ (i : ι), Real.exp (-β * 𝓒.energy i) ∂𝓒.μ) (-∫ (i : ι), 𝓒.energy i * Real.exp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.β) :

𝓒.meanEnergy T = -derivWithin (fun (β : ℝ) => Real.log (∫ (i : ι), Real.exp (-β * 𝓒.energy i) ∂𝓒.μ)) (Set.Ioi 0) ↑T.β

The mean energy is the negative derivative of the logarithm of the (mathematical) partition function with respect to β = 1/(kB T). see: Tong (§1.3.2, §1.3.3), L&L (§31, implicitly, and §36) Here the derivative is a derivWithin over Set.Ioi 0 since β > 0.

source

theorem CanonicalEnsemble.log_phys_eq_log_math_sub_const_on_Ioi {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) [NeZero 𝓒.μ] (h_fin : ∀ β > 0, MeasureTheory.IsFiniteMeasure (𝓒.μBolt (Temperature.ofβ β.toNNReal))) :

Set.EqOn (fun (β : ℝ) => Real.log (𝓒.partitionFunction (Temperature.ofβ β.toNNReal))) (fun (β : ℝ) => Real.log (∫ (i : ι), Real.exp (-β * 𝓒.energy i) ∂𝓒.μ) - ↑𝓒.dof * Real.log 𝓒.phaseSpaceunit) (Set.Ioi 0)

Helper: equality (on Set.Ioi 0) between the β–parametrized logarithm of the physical partition function and the β–parametrized logarithm of the mathematical partition function up to the (β–independent) semiclassical correction. This is used only to identify derivatives (the correction drops). We add the hypothesis h_fin giving finiteness of the Boltzmann measure for every β > 0 (as needed to ensure the mathematical partition function is strictly positive).

source

theorem CanonicalEnsemble.derivWithin_log_phys_eq_derivWithin_log_math {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hT_pos : 0 < T.val) [NeZero 𝓒.μ] (h_fin : ∀ β > 0, MeasureTheory.IsFiniteMeasure (𝓒.μBolt (Temperature.ofβ β.toNNReal))) :

derivWithin (fun (β : ℝ) => Real.log (𝓒.partitionFunction (Temperature.ofβ β.toNNReal))) (Set.Ioi 0) ↑T.β = derivWithin (fun (β : ℝ) => Real.log (∫ (i : ι), Real.exp (-β * 𝓒.energy i) ∂𝓒.μ)) (Set.Ioi 0) ↑T.β

Derivative equality needed in meanEnergy_eq_neg_deriv_log_Z_of_beta. Adds h_fin (finiteness of the Boltzmann measure for every β > 0).

source

theorem CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_Z_of_beta {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (hT_pos : 0 < T.val) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (h_fin : ∀ β > 0, MeasureTheory.IsFiniteMeasure (𝓒.μBolt (Temperature.ofβ β.toNNReal))) (h_deriv : HasDerivWithinAt (fun (β : ℝ) => ∫ (i : ι), Real.exp (-β * 𝓒.energy i) ∂𝓒.μ) (-∫ (i : ι), 𝓒.energy i * Real.exp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.β) :

𝓒.meanEnergy T = -derivWithin (fun (β : ℝ) => Real.log (𝓒.partitionFunction (Temperature.ofβ β.toNNReal))) (Set.Ioi 0) ↑T.β

The mean energy can also be expressed as the negative derivative of the logarithm of the physical partition function with respect to β. This follows from the fact that the physical and mathematical partition functions differ only by a constant factor, which vanishes upon differentiation.