def MicroHamiltonian.PartitionZ {D : Type} (H : MicroHamiltonian D) (d : D) (β : ℝ) : ℝ

The partition function corresponding to a given MicroHamiltonian. This is a function taking a thermodynamic β, not a temperature. It also depends on the data D defining the system extrinsincs.

• Ideally this would be an NNReal, but ∫ (NNReal) doesn't work right now, so it would just be a separate proof anyway

Equations

• H.PartitionZ d β = ∫ (config : H.dim d → ℝ), let E := H.H config; if h : E = ⊤ then 0 else Real.exp (-β * E.untop h)

def MicroHamiltonian.PartitionZT {D : Type} (H : MicroHamiltonian D) (d : D) (T : ℝ) : ℝ

The partition function as a function of temperature T instead of β.

Equations

• H.PartitionZT d T = H.PartitionZ d (1 / T)

def MicroHamiltonian.InternalU {D : Type} (H : MicroHamiltonian D) (d : D) (β : ℝ) : ℝ

The Internal Energy, U or E, defined as -∂(ln Z)/∂β. Parameterized here with β.

Equations

• H.InternalU d β = -deriv (fun (β' : ℝ) => Real.log (H.PartitionZ d β')) β

def MicroHamiltonian.HelmholtzA {D : Type} (H : MicroHamiltonian D) (d : D) (T : ℝ) : ℝ

The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not β.

Equations

• H.HelmholtzA d T = -T * Real.log (H.PartitionZT d T)

def MicroHamiltonian.EntropyS {D : Type} (H : MicroHamiltonian D) (d : D) (T : ℝ) : ℝ

The entropy, defined as the -∂A/∂T. Function of T.

Equations

• H.EntropyS d T = -deriv (H.HelmholtzA d) T

def MicroHamiltonian.EntropySβ {D : Type} (H : MicroHamiltonian D) (d : D) (β : ℝ) : ℝ

The entropy, defined as ln Z + β*U. Function of β.

Equations

• H.EntropySβ d β = Real.log (H.PartitionZ d β) + β * H.InternalU d β

def MicroHamiltonian.ZIntegrable {D : Type} (H : MicroHamiltonian D) (d : D) (β : ℝ) : Prop

To be able to compute or define anything from a Hamiltonian, we need its partition function to be a computable integral. A Hamiltonian is ZIntegrable at β if PartitionZ is Lesbegue integrable and nonzero.

Equations

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

def MicroHamiltonian.PositiveβIntegrable {D : Type} (H : MicroHamiltonian D) (d : D) : Prop

This Prop defines the most common case of ZIntegrable, that it is integrable at all finite temperatures (aka all positive β).

Equations

• H.PositiveβIntegrable d = ∀ β > 0, H.ZIntegrable d β

theorem MicroHamiltonian.DifferentiableAt_Z_if_ZIntegrable {D : Type} {H : MicroHamiltonian D} {d : D} {β : ℝ} (h : H.ZIntegrable d β) : ContDiffAt ℝ ⊤ (H.PartitionZ d) β

theorem MicroHamiltonian.entropy_A_eq_entropy_Z {D : Type} {H : MicroHamiltonian D} {d : D} (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegrable d β) : H.EntropyS d T = H.EntropySβ d β

The two definitions of entropy, in terms of T or β, are equivalent.

theorem MicroHamiltonian.β_eq_deriv_S_U {D : Type} {H : MicroHamiltonian D} {d : D} {β : ℝ} (hi : H.ZIntegrable d β) : β = deriv (H.EntropySβ d) β / deriv (H.InternalU d) β

The "definition of temperature from entropy": 1/T = (∂S/∂U), when the derivative is at constant extrinsic d (typically N/V). Here we use β instead of 1/T on the left, and express the right actually as (∂S/∂β)/(∂U/∂β), as all our things are ultimately parameterized by β.

def NVEHamiltonian.Pressure (H : NVEHamiltonian) (d : ℕ × ℝ) (T : ℝ) : ℝ

Pressure, as a function of T. Defined as the conjugate variable to volume.

Equations

• H.Pressure (n, V) T = -deriv (fun (V' : ℝ) => MicroHamiltonian.HelmholtzA H (n, V') T) V