Imports
/-
Copyright (c) 2025 Alex Meiburg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Meiburg
-/
module
public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantities
public import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransformIdeal gas as a Micro Canonical Ensemble
In this module we give the
@[expose] public sectionThe 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.
def IdealGas : NVEHamiltonian where
--The dimension of the manifold is 6 times the number of particles: three for position, three for
--momentum.
dim := fun (n,_) ↦ Fin n × (Fin 3 ⊕ Fin 3)
--The energy is ∞ if any positions are outside the cube, otherwise it's the sum of the momenta
--squared over 2.
H := fun {d} config ↦
let (n,V) := d
let R := V^(1/3:ℝ) / 2 --half-sidelength of a cubical box
if ∀ (i : Fin n) (ax : Fin 3), |config (i,.inl ax)| <= R then
∑ (i : Fin n) (ax : Fin 3), config (i,.inr ax)^2 / (2 : ℝ)
else
⊤
measurable_H := ⊢ ∀ (d : ℕ × ℝ),
Measurable fun config =>
match d, config with
| (n, V), config =>
let R := V ^ (1 / 3) / 2;
if ∀ (i : Fin n) (ax : Fin 3), |config (i, Sum.inl ax)| ≤ R then
∑ x ∈ Finset.univ ×ˢ Finset.univ,
match x with
| (i, ax) => ↑(config (i, Sum.inr ax) ^ 2 / 2)
else ⊤
n:ℕV:ℝ⊢ Measurable fun config =>
match (n, V), config with
| (n, V), config =>
let R := V ^ (1 / 3) / 2;
if ∀ (i : Fin n) (ax : Fin 3), |config (i, Sum.inl ax)| ≤ R then
∑ x ∈ Finset.univ ×ˢ Finset.univ,
match x with
| (i, ax) => ↑(config (i, Sum.inr ax) ^ 2 / 2)
else ⊤
n:ℕV:ℝ⊢ Measurable fun config =>
if ∀ (i : Fin n) (ax : Fin 3), |config (i, Sum.inl ax)| ≤ V ^ (1 / 3) / 2 then
∑ x, ↑(config (x.1, Sum.inr x.2) ^ 2 / 2)
else ⊤
n:ℕV:ℝ⊢ MeasurableSet {a | ∀ (i : Fin n) (ax : Fin 3), |a (i, Sum.inl ax)| ≤ V ^ (1 / 3) / 2}n:ℕV:ℝ⊢ Measurable fun config => ∑ x, ↑(config (x.1, Sum.inr x.2) ^ 2 / 2)
n:ℕV:ℝ⊢ MeasurableSet {a | ∀ (i : Fin n) (ax : Fin 3), |a (i, Sum.inl ax)| ≤ V ^ (1 / 3) / 2} simp_rw n:ℕV:ℝ⊢ MeasurableSet {a | ∀ (i : Fin n) (ax : Fin 3), |a (i, Sum.inl ax)| ≤ V ^ (1 / 3) / 2}n:ℕV:ℝ⊢ MeasurableSet (⋂ i, ⋂ i_1, {x | |x (i, Sum.inl i_1)| ≤ V ^ (1 / 3) / 2})]
exact MeasurableSet.iInter fun i => MeasurableSet.iInter fun ax =>
measurableSet_le (n:ℕV:ℝi:Fin nax:Fin 3⊢ Measurable fun x => |x (i, Sum.inl ax)| All goals completed! 🐙) measurable_const
n:ℕV:ℝ⊢ Measurable fun config => ∑ x, ↑(config (x.1, Sum.inr x.2) ^ 2 / 2) simp_rw n:ℕV:ℝ⊢ Measurable fun config => ∑ x, ↑(config (x.1, Sum.inr x.2) ^ 2 / 2)n:ℕV:ℝ⊢ Measurable fun config => ↑(∑ i, config (i.1, Sum.inr i.2) ^ 2 / 2)]
exact WithTop.isOpenEmbedding_coe.measurableEmbedding.measurable.comp (n:ℕV:ℝ⊢ Measurable fun config => ∑ i, config (i.1, Sum.inr i.2) ^ 2 / 2 All goals completed! 🐙)The Helmholtz Free Energy A for an ideal gas.
n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ -T * (↑n * Real.log V + 3 * ↑n / 2 * Real.log (2 * Real.pi * T)) =
-↑n * T * (Real.log V + 3 / 2 * Real.log (2 * Real.pi * T))n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ 0 < 2 * Real.pi / (1 / T)n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ V ^ n ≠ 0n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ (2 * Real.pi / (1 / T)) ^ (3 * ↑n / 2) ≠ 0
n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ 0 < 2 * Real.pi / (1 / T)n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ V ^ n ≠ 0n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ (2 * Real.pi / (1 / T)) ^ (3 * ↑n / 2) ≠ 0
all_goals All goals completed! 🐙n:ℕV:ℝβ:ℝhV:0 < Vhβ:0 < βhZpos:0 < partitionZ IdealGas (n, V) β⊢ partitionZ IdealGas (n, V) β ≠ 0
All goals completed! 🐙
n:ℕV:ℝβ:ℝhV:0 < Vhβ:0 < βhZpos:0 < partitionZ IdealGas (n, V) β⊢ partitionZ IdealGas (n, V) β ≠ 0 All goals completed! 🐙The ideal gas law: PV = nRT. In our unitsless system, R = 1.
n:ℕV:ℝT:ℝhV:0 < VhT:0 < Tx✝:ℝhV':x✝ ∈ Set.Ioi 0⊢ -↑n * T * (Real.log x✝ + 3 / 2 * Real.log (2 * Real.pi * T)) =
-(↑n * T * Real.log x✝) + ↑n * T * Real.log (T * Real.pi * 2) * (-3 / 2)
All goals completed! 🐙
n:ℕV:ℝT:ℝhV:0 < VhT:0 < T⊢ helmholtzA IdealGas (n, V) T = -↑n * T * (Real.log V + 3 / 2 * Real.log (2 * Real.pi * T)) All goals completed! 🐙-- Now proving e.g. Boyle's Law ("for an ideal gas with a fixed particle number, P and V are
-- inversely proportional") is a trivial consequence of the ideal gas law.
end IdealGas