1. Physlib
  2. StatisticalMechanics
  3. CanonicalEnsemble
  4. Lemmas
Imports
/- Copyright (c) 2025 Matteo Cipollina. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module public import Physlib.StatisticalMechanics.CanonicalEnsemble.Basic public import Mathlib.Analysis.SpecialFunctions.Log.Deriv

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.

@[expose] public sectionset_option linter.unusedVariables.funArgs false

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

lemma helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction (T : Temperature) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] : 𝓒.helmholtzFreeEnergy T = 𝓒.mathematicalHelmholtzFreeEnergy T + kB * T.val * 𝓒.dof * Real.log (𝓒.phaseSpaceunit) := ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μ⊢ 𝓒.helmholtzFreeEnergy T = 𝓒.mathematicalHelmholtzFreeEnergy T + kB * ↑T.val * ↑𝓒.dof * log 𝓒.phaseSpaceunit ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μ⊢ -kB * ↑T.val * (log (𝓒.mathematicalPartitionFunction T) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) = -kB * ↑T.val * log (𝓒.mathematicalPartitionFunction T) + kB * ↑T.val * ↑𝓒.dof * log 𝓒.phaseSpaceunit All goals completed! 🐙

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.

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhE:Integrable 𝓒.energy (𝓒.μProd T)h_log_prob:∀ (i : ι), log (𝓒.probability T i) = -↑T.β * 𝓒.energy i - log (𝓒.mathematicalPartitionFunction T)⊢ -kB * (-↑T.β * ∫ (a : ι), 𝓒.energy a ∂𝓒.μProd T - (𝓒.μProd T).real Set.univ • log (𝓒.mathematicalPartitionFunction T)) = kB * ↑T.β * ∫ (i : ι), 𝓒.energy i ∂𝓒.μProd T + kB * log (𝓒.mathematicalPartitionFunction T) ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhE:Integrable 𝓒.energy (𝓒.μProd T)h_log_prob:∀ (i : ι), log (𝓒.probability T i) = -↑T.β * 𝓒.energy i - log (𝓒.mathematicalPartitionFunction T)⊢ -kB * (-↑T.β * ∫ (a : ι), 𝓒.energy a ∂𝓒.μProd T - 1 * log (𝓒.mathematicalPartitionFunction T)) = kB * ↑T.β * ∫ (a : ι), 𝓒.energy a ∂𝓒.μProd T + kB * log (𝓒.mathematicalPartitionFunction T) All goals completed! 🐙

Pointwise logarithm of the Boltzmann probability.

lemma log_probability (𝓒 : CanonicalEnsemble ι) (T : Temperature) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (i : ι) : Real.log (𝓒.probability T i) = - (β T) * 𝓒.energy i - Real.log (𝓒.mathematicalPartitionFunction T) := ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μi:ι⊢ log (𝓒.probability T i) = -↑T.β * 𝓒.energy i - log (𝓒.mathematicalPartitionFunction T) All goals completed! 🐙

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

T:TemperaturehT:0 < T.valhT0:↑T.val ≠ 0⊢ kB * ↑T.β = 1 / ↑T.val T:TemperaturehT:0 < T.valhT0:↑T.val ≠ 0⊢ kB * ↑⟨1 / (kB * T.toReal), ⋯⟩ = 1 / ↑T.val T:TemperaturehT:0 < T.valhT0:↑T.val ≠ 0⊢ kB * (1 / (kB * ↑T.val)) = 1 / ↑T.val All goals completed! 🐙

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

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehE:Integrable 𝓒.energy (𝓒.μProd T)inst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μh_int_log_prob:Integrable (fun i => log (𝓒.probability T i)) (𝓒.μProd T)⊢ -kB * (∫ (a : ι), log (𝓒.probability T a) ∂𝓒.μProd T + (𝓒.μProd T).real Set.univ • (↑𝓒.dof * log 𝓒.phaseSpaceunit)) = -kB * ∫ (i : ι), log (𝓒.probability T i) ∂𝓒.μProd T - kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehE:Integrable 𝓒.energy (𝓒.μProd T)inst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μh_int_log_prob:Integrable (fun i => log (𝓒.probability T i)) (𝓒.μProd T)⊢ -kB * (∫ (a : ι), log (𝓒.probability T a) ∂𝓒.μProd T + 1 * (↑𝓒.dof * log 𝓒.phaseSpaceunit)) = -kB * ∫ (a : ι), log (𝓒.probability T a) ∂𝓒.μProd T - kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit All goals completed! 🐙

No semiclassical correction when dof = 0.

lemma thermodynamicEntropy_eq_differentialEntropy_of_dof_zero (T : Temperature) (hE : Integrable 𝓒.energy (𝓒.μProd T)) (h0 : 𝓒.dof = 0) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] : 𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T := ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehE:Integrable 𝓒.energy (𝓒.μProd T)h0:𝓒.dof = 0inst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μ⊢ 𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T All goals completed! 🐙

No semiclassical correction when phase_space_unit = 1.

lemma thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one (T : Temperature) (hE : Integrable 𝓒.energy (𝓒.μProd T)) (h1 : 𝓒.phaseSpaceunit = 1) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] : 𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T := ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehE:Integrable 𝓒.energy (𝓒.μProd T)h1:𝓒.phaseSpaceunit = 1inst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μ⊢ 𝓒.thermodynamicEntropy T = 𝓒.differentialEntropy T All goals completed! 🐙

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.

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT:0 < T.valinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhE:Integrable 𝓒.energy (𝓒.μProd T)hTne:↑T.val ≠ 0hkβT:↑T.val * (kB * ↑T.β) = 1⊢ -kB * ↑T.val * (log (𝓒.mathematicalPartitionFunction T) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) = 𝓒.meanEnergy T - ↑T.val * (kB * ↑T.β * 𝓒.meanEnergy T + kB * log (𝓒.mathematicalPartitionFunction T) - kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit) All goals completed! 🐙

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

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hTne:↑T.val ≠ 0⊢ 1 / ↑T.val * 𝓒.meanEnergy T + kB * log (𝓒.mathematicalPartitionFunction T) = (𝓒.meanEnergy T - -kB * ↑T.val * (log (𝓒.mathematicalPartitionFunction T) - ↑𝓒.dof * log 𝓒.phaseSpaceunit)) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hTne:↑T.val ≠ 0⊢ 𝓒.meanEnergy T + ↑T.val * kB * log (𝓒.mathematicalPartitionFunction T) = 𝓒.meanEnergy T - -(↑T.val * kB * (log (𝓒.mathematicalPartitionFunction T) - ↑𝓒.dof * log 𝓒.phaseSpaceunit)) + ↑T.val * kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit All goals completed! 🐙

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.

lemma differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp (𝓒 : CanonicalEnsemble ι) (T : Temperature) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hT : 0 < T.val) (hE : Integrable 𝓒.energy (𝓒.μProd T)) (hNorm : 𝓒.dof = 0 ∨ 𝓒.phaseSpaceunit = 1) : 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / T.val := ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hNorm:𝓒.dof = 0 ∨ 𝓒.phaseSpaceunit = 1⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hNorm:𝓒.dof = 0 ∨ 𝓒.phaseSpaceunit = 1hmain:𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunit⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hmain:𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunith:𝓒.dof = 0⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.valι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hmain:𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunith:𝓒.phaseSpaceunit = 1⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hmain:𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunith:𝓒.dof = 0⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.valι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μhT:0 < T.valhE:Integrable 𝓒.energy (𝓒.μProd T)hmain:𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val + kB * ↑𝓒.dof * log 𝓒.phaseSpaceunith:𝓒.phaseSpaceunit = 1⊢ 𝓒.differentialEntropy T = (𝓒.meanEnergy T - 𝓒.helmholtzFreeEnergy T) / ↑T.val All goals completed! 🐙

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

lemma 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 := (Real.hasDerivAt_log hx).comp_hasDerivWithinAt x hf

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

lemma 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 := f:ℝ → ℝf':ℝs:Set ℝx:ℝhf:HasDerivWithinAt f f' s xhx:f x ≠ 0⊢ HasDerivWithinAt (fun t => log (f t)) (1 / f x * f') s x All goals completed! 🐙
ι:Typeinst✝:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureφ:ι → ℝf:ι → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (-↑T.β * 𝓒.energy x))hf_meas:Measurable fhf_lt_top:∀ᵐ (x : ι) ∂𝓒.μ, f x < ∞⊢ ∫ (x : ι), φ x ∂𝓒.μ.withDensity f = ∫ (x : ι), φ x * rexp (-↑T.β * 𝓒.energy x) ∂𝓒.μ ι:Typeinst✝:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureφ:ι → ℝf:ι → ℝ≥0∞ := fun x => ENNReal.ofReal (rexp (-↑T.β * 𝓒.energy x))hf_meas:Measurable fhf_lt_top:∀ᵐ (x : ι) ∂𝓒.μ, f x < ∞h:∫ (x : ι), φ x ∂𝓒.μ.withDensity f = ∫ (x : ι), (f x).toReal • φ x ∂𝓒.μ⊢ ∫ (x : ι), φ x ∂𝓒.μ.withDensity f = ∫ (x : ι), φ x * rexp (-↑T.β * 𝓒.energy x) ∂𝓒.μ All goals completed! 🐙

A specialization of integral_bolt_eq_integral_mul_exp to the energy observable.

set_option linter.unusedVariables false inlemma integral_energy_bolt {ι} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) : ∫ x, 𝓒.energy x ∂ 𝓒.μBolt T = ∫ x, 𝓒.energy x * Real.exp (-T.β * 𝓒.energy x) ∂ 𝓒.μ := integral_bolt_eq_integral_mul_exp 𝓒 T 𝓒.energy

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

ι:Typeinst✝:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureh_den:((𝓒.μBolt T) Set.univ).toReal = ∫ (x : ι), rexp (-↑T.β * 𝓒.energy x) ∂𝓒.μ⊢ (∫ (x : ι), rexp (-↑T.β * 𝓒.energy x) ∂𝓒.μ)⁻¹ * ∫ (x : ι), 𝓒.energy x * rexp (-↑T.β * 𝓒.energy x) ∂𝓒.μ = (∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) / ∫ (i : ι), rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ All goals completed! 🐙

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.

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT_pos:0 < T.valinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μf:ℝ → ℝ := fun β => ∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μh_deriv:HasDerivWithinAt f (-∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.βhβ_pos:0 < ↑T.βhZpos:0 < f ↑T.βh_log:HasDerivWithinAt (fun β => log (f β)) (1 / f ↑T.β * -∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.βhUD:UniqueDiffWithinAt ℝ (Set.Ioi 0) ↑T.β⊢ (∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) / ∫ (i : ι), rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ = -(1 / f ↑T.β * -∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT_pos:0 < T.valinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μf:ℝ → ℝ := fun β => ∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μh_deriv:HasDerivWithinAt f (-∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.βhβ_pos:0 < ↑T.βhZpos:0 < f ↑T.βh_log:HasDerivWithinAt (fun β => log (f β)) (1 / f ↑T.β * -∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Set.Ioi 0) ↑T.βhUD:UniqueDiffWithinAt ℝ (Set.Ioi 0) ↑T.β⊢ (∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) / ∫ (i : ι), rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ = -((1 / ∫ (i : ι), rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) * -∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) All goals completed! 🐙

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

lemma log_phys_eq_log_math_sub_const_on_Ioi (𝓒 : CanonicalEnsemble ι) [NeZero 𝓒.μ] (h_fin : ∀ β > 0, IsFiniteMeasure (𝓒.μBolt (Temperature.ofβ (Real.toNNReal β)))) : Set.EqOn (fun β : ℝ => Real.log (𝓒.partitionFunction (Temperature.ofβ (Real.toNNReal β)))) (fun β : ℝ => Real.log (∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ) - (𝓒.dof : ℝ) * Real.log 𝓒.phaseSpaceunit) (Set.Ioi (0 : ℝ)) := ι:Typeinst✝¹:MeasurableSpace ι𝓒:CanonicalEnsemble ιinst✝:NeZero 𝓒.μh_fin:∀ β > 0, IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))⊢ EqOn (fun β => log (𝓒.partitionFunction (ofβ β.toNNReal))) (fun β => log (∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) (Ioi 0) ι:Typeinst✝¹:MeasurableSpace ι𝓒:CanonicalEnsemble ιinst✝:NeZero 𝓒.μh_fin:∀ β > 0, IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))β:ℝhβ:β ∈ Ioi 0⊢ (fun β => log (𝓒.partitionFunction (ofβ β.toNNReal))) β = (fun β => log (∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) β ι:Typeinst✝¹:MeasurableSpace ι𝓒:CanonicalEnsemble ιinst✝:NeZero 𝓒.μh_fin:∀ β > 0, IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))β:ℝhβ:β ∈ Ioi 0hβpos:0 < β⊢ (fun β => log (𝓒.partitionFunction (ofβ β.toNNReal))) β = (fun β => log (∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) β ι:Typeinst✝¹:MeasurableSpace ι𝓒:CanonicalEnsemble ιinst✝:NeZero 𝓒.μh_fin:∀ β > 0, IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))β:ℝhβ:β ∈ Ioi 0hβpos:0 < β_inst:IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))⊢ (fun β => log (𝓒.partitionFunction (ofβ β.toNNReal))) β = (fun β => log (∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ) - ↑𝓒.dof * log 𝓒.phaseSpaceunit) β All goals completed! 🐙

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

All goals completed! 🐙

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.

ι:Typeinst✝²:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT_pos:0 < T.valinst✝¹:IsFiniteMeasure (𝓒.μBolt T)inst✝:NeZero 𝓒.μh_fin:∀ β > 0, IsFiniteMeasure (𝓒.μBolt (ofβ β.toNNReal))h_deriv:HasDerivWithinAt (fun β => ∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ) (-∫ (i : ι), 𝓒.energy i * rexp (-↑T.β * 𝓒.energy i) ∂𝓒.μ) (Ioi 0) ↑T.β⊢ 𝓒.meanEnergy T = -derivWithin (fun β => log (∫ (i : ι), rexp (-β * 𝓒.energy i) ∂𝓒.μ)) (Ioi 0) ↑T.β All goals completed! 🐙

Fluctuations: variance identity

The identity Var(E) = ⟨E²⟩ - ⟨E⟩².

ι:Typeinst✝¹:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:Temperatureinst✝:IsProbabilityMeasure (𝓒.μProd T)hE_int:Integrable 𝓒.energy (𝓒.μProd T)hE2_int:Integrable (fun i => 𝓒.energy i ^ 2) (𝓒.μProd T)U:ℝ := ∫ (i : ι), 𝓒.energy i ∂𝓒.μProd ThU:U = ∫ (i : ι), 𝓒.energy i ∂𝓒.μProd Th_expand:(fun i => (𝓒.energy i - U) ^ 2) = fun i => 𝓒.energy i ^ 2 - 2 * U * 𝓒.energy i + U ^ 2h_int_E_mul_const:Integrable (fun i => 2 * U * 𝓒.energy i) (𝓒.μProd T)⊢ ∫ (a : ι), 𝓒.energy a ^ 2 ∂𝓒.μProd T - 2 * U * U + 1 * U ^ 2 = ∫ (i : ι), 𝓒.energy i ^ 2 ∂𝓒.μProd T - U ^ 2 All goals completed! 🐙

Heat capacity and parametric FDT

Relates C_V = dU/dT to dU/dβ. C_V = dU/dβ * (-1/(kB T²)).

ι:Typeinst✝:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT_pos:0 < T.valhU_deriv:HasDerivWithinAt 𝓒.meanEnergyBeta (derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β) (Set.Ioi 0) ↑T.βh_U_eq_comp:𝓒.meanEnergy_T = fun t => 𝓒.meanEnergyBeta (betaFromReal t)h_UD:UniqueDiffWithinAt ℝ (Set.Ioi 0) ↑T.val⊢ derivWithin (fun t => 𝓒.meanEnergyBeta (betaFromReal t)) (Set.Ioi 0) ↑T.val = derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β * (-1 / (kB * ↑T.val ^ 2)) All goals completed! 🐙

Parametric FDT: C_V = Var(E)/(kB T²), assuming Var(E) = - dU/dβ.

ι:Typeinst✝:MeasurableSpace ι𝓒:CanonicalEnsemble ιT:TemperaturehT_pos:0 < T.valh_Var_eq_neg_dUdβ:𝓒.energyVariance T = -derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.βhU_deriv:DifferentiableWithinAt ℝ 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β⊢ derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β * (-1 / (kB * ↑T.val ^ 2)) = -derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) ↑T.β / (kB * ↑T.val ^ 2) All goals completed! 🐙