PhysLean Documentation

PhysLean.StatisticalMechanics.CanonicalEnsemble.Lemmas

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 #

  1. Helmholtz Free Energies

  2. 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.
  3. Fundamental Thermodynamic Identity

    • Proof of F = U - T S_thermo.
    • Equivalent rearrangements giving entropy from energies and free energy.
    • Discrete / normalized specialization (no correction).
  4. Mean energy as U = - d/dβ log Z_math and likewise with the physical partition function (constant factor cancels).

Design Notes #

References #

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

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

Equations
Instances For

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

    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.

    Pointwise logarithm of the Boltzmann probability.

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

    The Fundamental Thermodynamic Identity #

    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.

    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).)

    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.

    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.

    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.

    theorem CanonicalEnsemble.integral_bolt_eq_integral_mul_exp {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (φ : ι) :
    (x : ι), φ x 𝓒.μBolt T = (x : ι), φ x * Real.exp (-T.β * 𝓒.energy x) 𝓒.μ
    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.

    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.

    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.

    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_integrable : β > 0, MeasureTheory.Integrable (fun (i : ι) => Real.exp (-β * 𝓒.energy i)) 𝓒.μ) (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.β) :

    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.