PhysLean Documentation

PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic

Canonical Ensemble: Core Definitions #

A canonical ensemble describes a system in thermal equilibrium with a heat bath at fixed temperature T. This file gives a measure–theoretic, semi–classical formalization intended to work uniformly for discrete (counting measure) and continuous (Lebesgue–type) models.

1. Semi–Classical Normalization #

Classical phase–space integrals produce dimensionful quantities. To obtain dimensionless thermodynamic objects (and an absolute entropy) we introduce:

The physical partition function is obtained from the mathematical one by dividing by phaseSpaceUnit ^ dof. This yields the standard semi–classical correction preventing ambiguities such as the Gibbs paradox.

2. Mathematical vs Physical Quantities #

We keep both layers:

Each physical quantity is expressed explicitly in terms of its mathematical ancestor.

3. Core Structure #

We assume phaseSpaceUnit > 0 and μ σ–finite. No probability assumption is imposed: normalization is recovered via the Boltzmann weighted measure.

4. Boltzmann & Probability Measures #

5. Energies & Entropies #

A helper lemma supplies positivity of the partition function under mild assumptions and non–negativity criteria for the entropy when probability ≤ 1 (automatic in finite discrete settings, not in general continuous ones).

6. Algebraic Operations #

We construct composite ensembles:

These operations respect partition functions, free energies, and (under suitable hypotheses) mean energies and integrability.

7. Notational & Implementation Notes #

8. References #

9. Roadmap #

Subsequent files (Lemmas.lean) prove:

A Canonical ensemble is described by a type ι, corresponding to the type of microstates, and a map ι → ℝ which associates which each microstate an energy and physical constants needed to define dimensionless thermodynamic quantities.

  • energy : ι

    The energy of associated with a mircrostate of the canonical ensemble.

  • dof :

    The number of degrees of freedom, used to make the partition function dimensionless. For a classical system of N particles in 3D, this is 3N. For a system of N spins, this is typically 0 as the state space is already discrete.

  • phaseSpaceunit :

    The unit of action used to make the phase space volume dimensionless. This constant is necessary to define an absolute (rather than relative) thermodynamic entropy. In the semi-classical approach, this unit is identified with Planck's constant h. For discrete systems with a counting measure, this unit should be set to 1.

  • hPos : 0 < self.phaseSpaceunit

    Assumption that the phase space unit is positive.

  • energy_measurable : Measurable self.energy
  • The measure on the indexing set of microstates.

  • μ_sigmaFinite : MeasureTheory.SigmaFinite self.μ
Instances For
    theorem CanonicalEnsemble.ext {ι : Type} [MeasurableSpace ι] {𝓒 𝓒' : CanonicalEnsemble ι} (h_energy : 𝓒.energy = 𝓒'.energy) (h_dof : 𝓒.dof = 𝓒'.dof) (h_h : 𝓒.phaseSpaceunit = 𝓒'.phaseSpaceunit) (h_μ : 𝓒.μ = 𝓒'.μ) :
    𝓒 = 𝓒'
    theorem CanonicalEnsemble.ext_iff {ι : Type} [MeasurableSpace ι] {𝓒 𝓒' : CanonicalEnsemble ι} :
    𝓒 = 𝓒' 𝓒.energy = 𝓒'.energy 𝓒.dof = 𝓒'.dof 𝓒.phaseSpaceunit = 𝓒'.phaseSpaceunit 𝓒.μ = 𝓒'.μ

    The addition of two CanonicalEnsemble. The degrees of freedom are added. Note: This is only physically meaningful if the two systems share the same phase_space_unit.

    Equations
    • One or more equations did not get rendered due to their size.

    The canonical ensemble with no microstates.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CanonicalEnsemble.congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) :

      Given a measurable equivalence e : ι1 ≃ᵐ ι, this is the corresponding canonical ensemble on ι1. The physical properties (dof, phase_space_unit) are unchanged.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CanonicalEnsemble.congr_energy_comp_symmm {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) :
        (𝓒.congr e).energy e.symm = 𝓒.energy
        noncomputable def CanonicalEnsemble.nsmul {ι : Type} [MeasurableSpace ι] (n : ) (𝓒 : CanonicalEnsemble ι) :

        Scalar multiplication of CanonicalEnsemble, defined such that nsmul n 𝓒 represents n non-interacting, distinguishable copies of the ensemble 𝓒.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]

          The microstates of a canonical ensemble.

          Equations
          Instances For

            Properties of physical parameters #

            @[simp]
            theorem CanonicalEnsemble.dof_add {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒1 : CanonicalEnsemble ι) (𝓒2 : CanonicalEnsemble ι1) :
            (𝓒1 + 𝓒2).dof = 𝓒1.dof + 𝓒2.dof
            @[simp]
            @[simp]
            theorem CanonicalEnsemble.dof_nsmul {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (n : ) :
            (nsmul n 𝓒).dof = n * 𝓒.dof
            @[simp]
            theorem CanonicalEnsemble.dof_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) :
            (𝓒.congr e).dof = 𝓒.dof

            The measure #

            theorem CanonicalEnsemble.μ_add {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) :
            (𝓒 + 𝓒1).μ = 𝓒.μ.prod 𝓒1.μ
            theorem CanonicalEnsemble.μ_nsmul {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (n : ) :
            (nsmul n 𝓒).μ = MeasureTheory.Measure.pi fun (x : Fin n) => 𝓒.μ

            The energy of the microstates #

            @[simp]
            theorem CanonicalEnsemble.energy_add_apply {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) (i : (𝓒 + 𝓒1).microstates) :
            (𝓒 + 𝓒1).energy i = 𝓒.energy i.1 + 𝓒1.energy i.2
            @[simp]
            theorem CanonicalEnsemble.energy_nsmul_apply {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (n : ) (f : Fin n𝓒.microstates) :
            (nsmul n 𝓒).energy f = i : Fin n, 𝓒.energy (f i)
            @[simp]
            theorem CanonicalEnsemble.energy_congr_apply {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (i : ι1) :
            (𝓒.congr e).energy i = 𝓒.energy (e i)

            Induction for nsmul #

            theorem CanonicalEnsemble.nsmul_succ {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (n : ) [MeasureTheory.SigmaFinite 𝓒.μ] :
            nsmul n.succ 𝓒 = (𝓒 + nsmul n 𝓒).congr (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => ι) 0)

            Non zero nature of the measure #

            instance CanonicalEnsemble.instNeZeroMeasureProdμHAdd {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) [NeZero 𝓒.μ] [NeZero 𝓒1.μ] :
            NeZero (𝓒 + 𝓒1).μ
            instance CanonicalEnsemble.μ_neZero_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) [NeZero 𝓒.μ] (e : ι1 ≃ᵐ ι) :
            NeZero (𝓒.congr e).μ

            The Boltzmann measure #

            The Boltzmann measure on the space of microstates.

            Equations
            Instances For
              @[simp]
              theorem CanonicalEnsemble.μBolt_add {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) (T : Temperature) :
              (𝓒 + 𝓒1).μBolt T = (𝓒.μBolt T).prod (𝓒1.μBolt T)
              theorem CanonicalEnsemble.μBolt_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (T : Temperature) :
              (𝓒.congr e).μBolt T = MeasureTheory.Measure.map (⇑e.symm) (𝓒.μBolt T)

              The Mathematical Partition Function #

              The mathematical partition function, defined as the integral of the Boltzmann factor. This quantity may have physical dimensions. See CanonicalEnsemble.partitionFunction for the dimensionless physical version.

              Equations
              Instances For

                The partition function is strictly positive provided the underlying measure is non-zero and the Boltzmann measure is finite.

                The probability density #

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

                The probability density function of the canonical ensemble. Note: In the general measure-theoretic case, this is a density with respect to the underlying measure 𝓒.μ and is not necessarily less than or equal to 1. In the case of a finite ensemble with the counting measure, this value corresponds to the probability of the microstate.

                Equations
                Instances For

                  The probability measure #

                  theorem CanonicalEnsemble.probability_add {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) {T : Temperature} (i : ι × ι1) :
                  (𝓒 + 𝓒1).probability T i = 𝓒.probability T i.1 * 𝓒1.probability T i.2
                  @[simp]
                  theorem CanonicalEnsemble.probability_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (T : Temperature) (i : ι1) :
                  (𝓒.congr e).probability T i = 𝓒.probability T (e i)
                  theorem CanonicalEnsemble.probability_nsmul {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (n : ) (T : Temperature) (f : Fin nι) :
                  (nsmul n 𝓒).probability T f = i : Fin n, 𝓒.probability T (f i)

                  The probability measure associated with the Boltzmann distribution of a canonical ensemble.

                  Equations
                  Instances For
                    theorem CanonicalEnsemble.μProd_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (T : Temperature) :
                    (𝓒.congr e).μProd T = MeasureTheory.Measure.map (⇑e.symm) (𝓒.μProd T)

                    Integrability of energy #

                    The mean energy #

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

                    The mean energy of the canonical ensemble at temperature T.

                    Equations
                    Instances For
                      theorem CanonicalEnsemble.meanEnergy_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (T : Temperature) :
                      (𝓒.congr e).meanEnergy T = 𝓒.meanEnergy T

                      The differential entropy #

                      The (differential) entropy of the canonical ensemble. In the continuous case, this quantity is not absolute but depends on the choice of units for the measure. It can be negative. See thermodynamicEntropy for the absolute physical quantity.

                      Equations
                      Instances For

                        Probabilities are non-negative, assuming a positive partition function.

                        Probabilities are strictly positive.

                        theorem CanonicalEnsemble.differentialEntropy_nonneg_of_prob_le_one {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [MeasureTheory.IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (hInt : MeasureTheory.Integrable (fun (i : ι) => Real.log (𝓒.probability T i)) (𝓒.μProd T)) (hP_le_one : ∀ (i : ι), 𝓒.probability T i 1) :

                        General entropy non-negativity under a pointwise upper bound probability ≤ 1. This assumption holds automatically in the finite/counting case (since sums bound each term), but can fail in general (continuous) settings; hence we separate it as a hypothesis. Finite case: see CanonicalEnsemble.entropy_nonneg in Finite.

                        Thermodynamic Quantities #

                        These are the dimensionless physical quantities derived from the mathematical definitions by incorporating the phase space volume 𝓒.phaseSpaceUnit ^ 𝓒.dof.

                        The dimensionless thermodynamic partition function, Z = Z_math / h^dof.

                        Equations
                        Instances For

                          A rewriting form convenient under a coercion to a temperature obtained from an inverse temperature.

                          The logarithm of the mathematical partition function as an integral.

                          The Helmholtz free energy, F = -k_B T log(Z). This is the central quantity from which other thermodynamic properties are derived.

                          Equations
                          Instances For
                            noncomputable def CanonicalEnsemble.physicalProbability {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) (i : ι) :

                            The dimensionless physical probability density. This is is the probability density w.r.t. the measure, obtained by dividing the phase space measure by the fundamental unit h^dof, making the probability density ρ_phys = ρ_math * h^dof dimensionless.

                            Equations
                            Instances For

                              Normalization of the dimensionless physical probability density over the base measure.

                              theorem CanonicalEnsemble.physicalProbability_congr {ι ι1 : Type} [MeasurableSpace ι] [MeasurableSpace ι1] (𝓒 : CanonicalEnsemble ι) (e : ι1 ≃ᵐ ι) (T : Temperature) (i : ι1) :
                              theorem CanonicalEnsemble.physicalProbability_add {ι : Type} [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) {ι1 : Type} [MeasurableSpace ι1] (𝓒1 : CanonicalEnsemble ι1) (T : Temperature) (i : ι × ι1) (h : 𝓒.phaseSpaceunit = 𝓒1.phaseSpaceunit) :
                              (𝓒 + 𝓒1).physicalProbability T i = 𝓒.physicalProbability T i.1 * 𝓒1.physicalProbability T i.2

                              The absolute thermodynamic entropy, defined from its statistical mechanical foundation as the Gibbs-Shannon entropy of the dimensionless physical probability distribution. This corresponds to Landau & Lifshitz, Statistical Physics, §7, Eq. 7.12.

                              Equations
                              Instances For