Two-state canonical ensemble

This module contains the definitions and properties related to the two-state canonical ensemble.

def CanonicalEnsemble.twoState (E : ℝ) : CanonicalEnsemble (Fin 2)

The canonical ensemble corresponding to state system, with one state of energy E and the other state of energy 0.

Equations

• CanonicalEnsemble.twoState E 0 = 0
• CanonicalEnsemble.twoState E 1 = E

theorem CanonicalEnsemble.twoState_partitionFunction_apply_eq_one_add_exp (E : ℝ) (T : Temperature) : (twoState E).partitionFunction T = 1 + Real.exp (-T.β * E)

theorem CanonicalEnsemble.twoState_partitionFunction_apply_eq_cosh (E : ℝ) (T : Temperature) : (twoState E).partitionFunction T = 2 * Real.exp (-T.β * E / 2) * Real.cosh (T.β * E / 2)

theorem CanonicalEnsemble.twoState_partitionFunctionβ_eq (E : ℝ) : (twoState E).partitionFunctionβ = fun (β : ℝ) => 2 * Real.exp (-β * E / 2) * Real.cosh (β * E / 2)

theorem CanonicalEnsemble.twoState_meanEnergy_eq (E : ℝ) (T : Temperature) : (twoState E).meanEnergy T = E / 2 * (1 - Real.tanh (T.β * E / 2))

def CanonicalEnsemble.twoState_entropy_eq : InformalLemma

A simplification of the entropy of the two-state canonical ensemble.

Equations

• CanonicalEnsemble.twoState_entropy_eq = { deps := [`CanonicalEnsemble.twoState, `CanonicalEnsemble.entropy], tag := "EVJJI" }

def CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq : InformalLemma

A simplification of the helmholtzFreeEnergy of the two-state canonical ensemble.

Equations

• CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq = { deps := [`CanonicalEnsemble.twoState, `CanonicalEnsemble.helmholtzFreeEnergy], tag := "EVMPR" }