Statistical Mechanics

Stream: PhysLean

[Joseph Tooby-Smith]

Just came across these notes of David Tong's:

https://www.damtp.cam.ac.uk/user/tong/statphys/statmechhtml/S1.html

Seems like section 1.3 on canonical ensembles would be pretty nice to work through and formalized. If this isn't something that already exists somewhere in Lean which would could upstream?

[Joseph Tooby-Smith]

This PR contains the basic definitions of the canonical ensemble along with some properties.

[Joseph Tooby-Smith]

As part of the above PR I've added a number of semi-formal results, e.g.

• semiformal_result (ERA5D): partitionFunction_nsmul
• semiformal_result (ERBG6): probability_nsmul

most of which are related to multiples of a canonical ensemble.

Semi-formal results are essentially the same as proof_wanted results, where the statement is formalized but the proof hasn't. If anyone wants to have a go at these that would be great.

[Joseph Tooby-Smith]

The corresponding file with these semi-formal results can be interacted with online at:

https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FStatisticalMechanics%2FCanonicalEnsemble%2FBasic.lean

[Matteo Cipollina]

In this large PR we expand the API in CanonicalEnsemble and provide additional properties. I just paste below the PR description in case anyone want to review it before we merge.
--
This PR refines the general measure-theoretic framework for the canonical ensemble, applicable to both classical continuous systems (like an ideal gas) and discrete systems (like a spin lattice). It introduces additional parameters to the CanonicalEnsemble structure and various distinctions between entropy and proves some key thermodynamics identities.

We follow the semi-classical approach in Landau-Lefschetz and also in Tong's lecture notes in designing a general API (for this initial level of analysis) to handle both discrete and continuous systems. The explicitation of a classical principled exposition like L&L constrained us to distinguish two layers:

Mathematical layer: Raw partition function ∫ exp(-βE) dμ, probability densities w.r.t. base measure
Physical layer: Dimensionless thermodynamic quantities via phaseSpaceUnit^dof normalization

This seems to be a more clear way to analyze the presuppositions of the classical theory that pre-empt ambiguity issues (Gibbs paradox) by making entropy absolute rather than relative.

Main additions :

New parameters to the CanonicalEnsemble structure:

• phaseSpaceUnit : ℝ (physically Planck's constant h)
• dof : ℕ (degrees of freedom)

Thermodynamic quantities:

• partitionFunction = mathematicalPartitionFunction / h^dof
• helmholtzFreeEnergy = -kT log Z
• thermodynamicEntropy (absolute) vs differentialEntropy (can be negative)
• physicalProbability = probability * h^dof (dimensionless)

Main results and corollaries from L&L and Tong's notes that we prove in the fileLemmas are:

• Fundamental identity: F = U - TS (theorem helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy)
• Response formula*: U = -∂log Z/∂β (theorem meanEnergy_eq_neg_deriv_log_mathZ_of_beta)
• Entropy relations: S_thermo = S_diff - k·dof·log h with semi-classical correction

Finite case (IsFinite) specializations

Specialization where dof = 0, phaseSpaceUnit = 1, where we show:

• Shannon entropy = differential entropy = thermodynamic entropy
• No semi-classical corrections needed
• Unconditional entropy non-negativity

As designed here the introduction of this necessary semi-classical correction k·dof·log h appears systematically where needed and vanishes in the discrete case.

[Joseph Tooby-Smith]

Many thanks for all the work you put into this @Matteo Cipollina !