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
orphaseSpaceUnit = 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).
- Proof of
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
onSet.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
.
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
.
No semiclassical correction when dof = 0
.
No semiclassical correction when phase_space_unit = 1
.
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.
Chain rule convenience lemma for log ∘ f
on a set.
A version rewriting the derivative value with 1 / f x
.
A specialization of integral_bolt_eq_integral_mul_exp
to the energy observable.
The mean energy can be expressed as a ratio of integrals.
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
.
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.