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

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

def CanonicalEnsemble (ι : Type) : Type

A Canonical ensemble is described by a type ι, corresponding to the type of microstates, and a map ι → ℝ which associates which each microstate an energy.

Equations

• CanonicalEnsemble ι = (ι → ℝ)

instance CanonicalEnsemble.instHAddProd {ι1 ι2 : Type} : HAdd (CanonicalEnsemble ι1) (CanonicalEnsemble ι2) (CanonicalEnsemble (ι1 × ι2))

The addition of two CanonicalEnsemble.

Equations

• CanonicalEnsemble.instHAddProd = { hAdd := fun (𝓒1 : CanonicalEnsemble ι1) (𝓒2 : CanonicalEnsemble ι2) (i : ι1 × ι2) => 𝓒1 i.1 + 𝓒2 i.2 }

def CanonicalEnsemble.nsmul {ι : Type} (n : ℕ) (𝓒1 : CanonicalEnsemble ι) : CanonicalEnsemble (Fin n → ι)

Scalar multiplication of CanonicalEnsemble, defined such that nsmul n 𝓒 is n coppies of the canonical ensemble 𝓒.

Equations

• CanonicalEnsemble.nsmul n 𝓒1 f = ∑ i : Fin n, 𝓒1 (f i)

@[reducible, inline]

abbrev CanonicalEnsemble.microstates {ι : Type} (𝓒 : CanonicalEnsemble ι) : Type

The microstates of a the canonical ensemble

Equations

• 𝓒.microstates = ι

The energy of the microstates

@[reducible, inline]

abbrev CanonicalEnsemble.energy {ι : Type} (𝓒 : CanonicalEnsemble ι) : 𝓒.microstates → ℝ

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

Equations

• 𝓒.energy = 𝓒

@[simp]

theorem CanonicalEnsemble.energy_add_apply {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) (i : (𝓒 + 𝓒1).microstates) : (𝓒 + 𝓒1).energy i = 𝓒.energy i.1 + 𝓒1.energy i.2

@[simp]

theorem CanonicalEnsemble.energy_nsmul_apply {ι : Type} (𝓒 : CanonicalEnsemble ι) (n : ℕ) (f : Fin n → 𝓒.microstates) : (nsmul n 𝓒).energy f = ∑ i : Fin n, 𝓒.energy (f i)

The partition function of the canonical ensemble

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

The partition function of the canonical ensemble.

Equations

• 𝓒.partitionFunction T = ∑ i : 𝓒.microstates, Real.exp (-T.β * 𝓒.energy i)

theorem CanonicalEnsemble.partitionFunction_add {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) {T : Temperature} [Fintype ι] [Fintype ι1] : (𝓒 + 𝓒1).partitionFunction T = 𝓒.partitionFunction T * 𝓒1.partitionFunction T

theorem CanonicalEnsemble.partitionFunction_pos {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (T : Temperature) : 0 < 𝓒.partitionFunction T

@[simp]

theorem CanonicalEnsemble.partitionFunction_neq_zero {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (T : Temperature) : 𝓒.partitionFunction T ≠ 0

noncomputable def CanonicalEnsemble.partitionFunctionβ {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] (β : ℝ) : ℝ

The partition function of the canonical ensemble as a function of β

Equations

• 𝓒.partitionFunctionβ β = ∑ i : 𝓒.microstates, Real.exp (-β * 𝓒.energy i)

theorem CanonicalEnsemble.partitionFunctionβ_def {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] : 𝓒.partitionFunctionβ = fun (β : ℝ) => ∑ i : 𝓒.microstates, Real.exp (-β * 𝓒.energy i)

theorem CanonicalEnsemble.partitionFunctionβ_differentiable {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] : Differentiable ℝ 𝓒.partitionFunctionβ

theorem CanonicalEnsemble.partitionFunction_eq_partitionFunctionβ {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] (T : Temperature) : 𝓒.partitionFunction T = 𝓒.partitionFunctionβ T.β

The probability of being in a given microstate

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

The probability of been in a given microstate.

Equations

• 𝓒.probability i T = Real.exp (-T.β * 𝓒.energy i) / 𝓒.partitionFunction T

theorem CanonicalEnsemble.probability_neq_zero {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (i : 𝓒.microstates) (T : Temperature) : 𝓒.probability i T ≠ 0

@[simp]

theorem CanonicalEnsemble.probability_add {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) [Fintype ι] [Fintype ι1] (i : (𝓒 + 𝓒1).microstates) (T : Temperature) : (𝓒 + 𝓒1).probability i T = 𝓒.probability i.1 T * 𝓒1.probability i.2 T

@[simp]

theorem CanonicalEnsemble.sum_probability_eq_one {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (T : Temperature) : ∑ i : 𝓒.microstates, 𝓒.probability i T = 1

The mean energy of the canonical ensemble

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

The mean energy of the canonical ensemble.

Equations

• 𝓒.meanEnergy T = ∑ i : 𝓒.microstates, 𝓒.energy i * 𝓒.probability i T

@[simp]

theorem CanonicalEnsemble.meanEnergy_add {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (𝓒1 : CanonicalEnsemble ι1) [Fintype ι1] [Nonempty ι1] (T : Temperature) : (𝓒 + 𝓒1).meanEnergy T = 𝓒.meanEnergy T + 𝓒1.meanEnergy T

theorem CanonicalEnsemble.meanEnergy_eq_logDeriv_partitionFunctionβ {ι : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] (T : Temperature) : 𝓒.meanEnergy T = -logDeriv 𝓒.partitionFunctionβ T.β

Entropy

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

The entropy of the canonical ensemble.

Equations

• 𝓒.entropy T = -↑Constants.kB * ∑ i : 𝓒.microstates, 𝓒.probability i T * Real.log (𝓒.probability i T)

@[simp]

theorem CanonicalEnsemble.entropy_add {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) [Fintype ι] [Nonempty ι] (𝓒1 : CanonicalEnsemble ι1) [Fintype ι1] [Nonempty ι1] (T : Temperature) : (𝓒 + 𝓒1).entropy T = 𝓒.entropy T + 𝓒1.entropy T

Entropy is addative on adding canonical ensembles.

Helmholtz free energy

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

The (Helmholtz) free energy of the canonical ensemble.

Equations

• 𝓒.helmholtzFreeEnergy T = 𝓒.meanEnergy T - T.toReal * 𝓒.entropy T

@[simp]

theorem CanonicalEnsemble.helmholtzFreeEnergy_add {ι ι1 : Type} (𝓒 : CanonicalEnsemble ι) (𝓒1 : CanonicalEnsemble ι1) [Fintype ι] [Nonempty ι] [Fintype ι1] [Nonempty ι1] (T : Temperature) : (𝓒 + 𝓒1).helmholtzFreeEnergy T = 𝓒.helmholtzFreeEnergy T + 𝓒1.helmholtzFreeEnergy T

The Helmholtz free energy is addative.