PhysLean Documentation

PhysLean.StatisticalMechanics.CanonicalEnsemble.Finite

Finite canonical ensemble #

A canonical ensemble describes a system in thermal equilibrium with a heat bath at a fixed temperature.

In this file we define the canonical ensemble, its partition function, the probability of being in a given microstate, the mean energy, the entropy and the Helmholtz free energy.

We also define the addition of two canonical ensembles, and prove results related to the properties of additions of canonical ensembles.

## References

Implementation note #

This file only deals with finite canonical ensembles. When the more general theory of canonical ensembles is implemented, this file should be modified.

A finite CanonicalEnsemble is one whose microstates form a finite type and whose measure is the counting measure. For such systems, the state space is inherently discrete and dimensionless, so we require dof = 0 and phaseSpaceUnit = 1.

Instances
    instance CanonicalEnsemble.instIsFiniteCongr {ι : Type} [Fintype ι] [MeasurableSpace ι] (𝓒 : CanonicalEnsemble ι) {ι1 : Type} [Fintype ι1] [MeasurableSpace ι1] [𝓒.IsFinite] (e : ι1 ≃ᵐ ι) :
    (𝓒.congr e).IsFinite

    In the finite (counting) case a nonempty index type gives a nonzero measure.

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

    The Shannon entropy of a finite canonical ensemble. This is defined by the formula S = -k_B ∑ pᵢ log pᵢ. It is proven to be equivalent to the differentialEntropy and the thermodynamicEntropy for systems satisfying the IsFinite property.

    Equations
    Instances For
      @[simp]
      theorem CanonicalEnsemble.μBolt_of_fintype {ι : Type} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (𝓒 : CanonicalEnsemble ι) (T : Temperature) [𝓒.IsFinite] (i : ι) :
      (𝓒.μBolt T).real {i} = Real.exp (-T.β * 𝓒.energy i)
      @[simp]

      Finite specialization: strict positivity of the mathematical partition function.

      Finite specialization: strict positivity of the (physical) partition function.

      Finite specialization: non-negativity (indeed positivity) of probabilities.

      The sum of probabilities over all microstates is 1.

      The entropy of a finite canonical ensemble (Shannon entropy) is non-negative.

      In the finite, nonempty case the thermodynamic and Shannon entropies coincide. All semi-classical correction factors vanish (dof = 0, phaseSpaceUnit = 1), so the absolute thermodynamic entropy reduces to the discrete Shannon form.