def IdealGas : NVEHamiltonian

The Hamiltonian for an ideal gas: particles live in a cube of volume V^(1/3), and each contributes an energy p^2/2. The per-particle mass is normalized to 1.

Equations

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

theorem IdealGas.PartitionZ_eq (n : ℕ) {V β : ℝ} (hV : 0 < V) (hβ : 0 < β) : MicroHamiltonian.PartitionZ IdealGas (n, V) β = V ^ n * (2 * Real.pi / β) ^ (3 * ↑n / 2)

The partition function Z for an ideal gas.

theorem IdealGas.HelmholtzA_eq (n : ℕ) {V T : ℝ} (hV : 0 < V) (hT : 0 < T) : MicroHamiltonian.HelmholtzA IdealGas (n, V) T = -↑n * T * (Real.log V + 3 / 2 * Real.log (2 * Real.pi * T))

The Helmholtz Free Energy A for an ideal gas.

theorem IdealGas.ZIntegrable (n : ℕ) {V β : ℝ} (hV : 0 < V) (hβ : 0 < β) : MicroHamiltonian.ZIntegrable IdealGas (n, V) β

theorem IdealGas.IdealGasLaw (n : ℕ) {V T : ℝ} (hV : 0 < V) (hT : 0 < T) : let P := IdealGas.Pressure (n, V) T; let R := 1; P * V = ↑n * R * T

The ideal gas law: PV = nRT. In our unitsless system, R = 1.