From 74fb28e121c505f1e2eb74375f521d810d4644df Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 6 May 2026 11:43:07 +0100 Subject: [PATCH 1/4] refactor: Move statmech --- Physlib.lean | 3 + .../MicroCanonicalEnsemble/Basic.lean | 50 ++++++++ .../MicroCanonicalEnsemble}/IdealGas.lean | 81 ++++++------- .../ThermoQuantities.lean | 110 +++++++++--------- QuantumInfo.lean | 5 - QuantumInfo/StatMech/Hamiltonian.lean | 42 ------- scripts/lint_all.lean | 1 + 7 files changed, 153 insertions(+), 139 deletions(-) create mode 100644 Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean rename {QuantumInfo/StatMech => Physlib/StatisticalMechanics/MicroCanonicalEnsemble}/IdealGas.lean (79%) rename {QuantumInfo/StatMech => Physlib/StatisticalMechanics/MicroCanonicalEnsemble}/ThermoQuantities.lean (64%) delete mode 100644 QuantumInfo/StatMech/Hamiltonian.lean diff --git a/Physlib.lean b/Physlib.lean index 19fd8fe2b..bcf0af804 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -382,6 +382,9 @@ public import Physlib.StatisticalMechanics.CanonicalEnsemble.Basic public import Physlib.StatisticalMechanics.CanonicalEnsemble.Finite public import Physlib.StatisticalMechanics.CanonicalEnsemble.Lemmas public import Physlib.StatisticalMechanics.CanonicalEnsemble.TwoState +public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.Basic +public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.IdealGas +public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantities public import Physlib.StringTheory.Basic public import Physlib.StringTheory.FTheory.SU5.Basic public import Physlib.StringTheory.FTheory.SU5.Charges.AnomalyFree diff --git a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean new file mode 100644 index 000000000..25a7803fe --- /dev/null +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/Basic.lean @@ -0,0 +1,50 @@ +/- +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 Mathlib.Data.Fintype.Defs +public import Mathlib.Data.Real.Basic +public import Physlib.Meta.Sorry +/-! + +## The Microcanonical Ensemble + +-/ + +@[expose] public section + +section ThermodynamicEnsemble + +/-- The Hamiltonian for a microcanonical ensemble, parameterized by any extrinsic parameters of data + D. Since it's an arbitrary type, 'T' would be nice, but we use 'D' for data to avoid confusion + with temperature. We define Hamiltonians as an energy function on a real manifold, whose + dimension n possibly depends on the data D. Energy is a WithTop ℝ, ⊤ is used to mean "excluded + as a possibility in phase space". This formalization does exclude the possibility of discrete + degrees of freedom; it is not _completely_ general. A better formalization could have an + arbitrary measurable space. +-/ +structure MicroHamiltonian (D : Type) where + /-- For extrinsic parameters D (e.g. the number of particles of different chemical species, + the shape of the box), how many continuous degrees of freedom are there? -/ + dim : D → Type + /-- We require that the number of degrees of freedom is finite. -/ + [dim_fin : ∀ d, Fintype (dim d)] + /-- Given the configuration, what is its energy? -/ + H : {d : D} → (dim d → ℝ) → WithTop ℝ + +/-- We add the dim_fin to the instance cache so that things like the measure can be synthesized -/ +instance microHamiltonianFintype {D} (H : MicroHamiltonian D) (d : D) : Fintype (H.dim d) := + H.dim_fin d + +/-- The standard microcanonical ensemble Hamiltonian, where the data is the particle number N and + the volume V. -/ +abbrev NVEHamiltonian := MicroHamiltonian (ℕ × ℝ) + +/-- Helper to get the number in an N-V Hamiltonian -/ +def NVEHamiltonian.N : (ℕ × ℝ) → ℕ := Prod.fst + +/-- Helper to get the volume in an N-V Hamiltonian -/ +def NVEHamiltonian.V : (ℕ × ℝ) → ℝ := Prod.snd diff --git a/QuantumInfo/StatMech/IdealGas.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean similarity index 79% rename from QuantumInfo/StatMech/IdealGas.lean rename to Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean index 9128f61a9..a73e8f96a 100644 --- a/QuantumInfo/StatMech/IdealGas.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean @@ -5,21 +5,28 @@ Authors: Alex Meiburg -/ module -public import QuantumInfo.StatMech.ThermoQuantities +public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.ThermoQuantities public import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform +/-! +## Ideal gas as a Micro Canonical Ensemble + +In this module we give the +-/ @[expose] public section noncomputable section --! Specializing to an ideal gas of distinguishable particles. -/-- 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. -/ +/-- 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. -/ def IdealGas : NVEHamiltonian where - --The dimension of the manifold is 6 times the number of particles: three for position, three for momentum. + --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. + --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 @@ -37,28 +44,30 @@ variable (n : ℕ) {V β T : ℝ} set_option backward.isDefEq.respectTransparency false in open MeasureTheory in /-- The partition function Z for an ideal gas. -/ -theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : - IdealGas.PartitionZ (n,V) β = V^n * (2 * Real.pi / β)^(3 * n / 2 : ℝ) := by - rw [PartitionZ, IdealGas] +lemma partitionZ_eq (hV : 0 < V) (hβ : 0 < β) : + IdealGas.partitionZ (n,V) β = V ^ n * (2 * Real.pi / β) ^ (3 * n / 2 : ℝ) := by + rw [partitionZ, IdealGas] simp only [Finset.univ_product_univ, one_div, ite_eq_right_iff, WithTop.sum_eq_top, Finset.mem_univ, WithTop.coe_ne_top, and_false, exists_false, imp_false, not_forall, not_le, neg_mul] have h₀ : ∀ (config:Fin n × (Fin 3 ⊕ Fin 3) → ℝ) proof, ((if ∀ (i : Fin n) (ax : Fin 3), |config (i, Sum.inl ax)| ≤ V ^ (3 : ℝ)⁻¹ / 2 then ∑ x : Fin n × Fin 3, config (x.1, Sum.inr x.2) ^ 2 / (2 :ℝ) - else ⊤) : WithTop ℝ).untop proof = ∑ x : Fin n × Fin 3, config (x.1, Sum.inr x.2) ^ 2 / (2 :ℝ) := by + else ⊤) : WithTop ℝ).untop proof = + ∑ x : Fin n × Fin 3, config (x.1, Sum.inr x.2) ^ 2 / (2 :ℝ) := by intro config proof rw [WithTop.untop_eq_iff] split_ifs with h · simp · simp [h] at proof simp only [h₀, dite_eq_ite]; clear h₀ - - let eq_pm : MeasurableEquiv ((Fin n × Fin 3 → ℝ) × (Fin n × Fin 3 → ℝ)) (Fin n × (Fin 3 ⊕ Fin 3) → ℝ) := - let e1 := (MeasurableEquiv.sumPiEquivProdPi (α := fun (_ : (Fin n × Fin 3) ⊕ (Fin n × Fin 3)) ↦ ℝ)) - let e2 := (MeasurableEquiv.piCongrLeft _ (MeasurableEquiv.prodSumDistrib (Fin n) (Fin 3) (Fin 3))).symm + let eq_pm : MeasurableEquiv ((Fin n × Fin 3 → ℝ) × + (Fin n × Fin 3 → ℝ)) (Fin n × (Fin 3 ⊕ Fin 3) → ℝ) := + let e1 := (MeasurableEquiv.sumPiEquivProdPi + (α := fun (_ : (Fin n × Fin 3) ⊕ (Fin n × Fin 3)) ↦ ℝ)) + let e2 := (MeasurableEquiv.piCongrLeft _ + (MeasurableEquiv.prodSumDistrib (Fin n) (Fin 3) (Fin 3))).symm e1.symm.trans e2 - have h_preserve : MeasurePreserving eq_pm := by unfold eq_pm -- fun_prop --this *should* be a fun_prop! @@ -69,16 +78,13 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : · apply MeasurePreserving.symm apply measurePreserving_sumPiEquivProdPi rw [← MeasurePreserving.integral_comp h_preserve eq_pm.measurableEmbedding]; clear h_preserve - rw [show volume = Measure.prod volume volume from rfl] - have h_eval_eq_pm : ∀ (x y i p_i), eq_pm (x, y) (i, Sum.inl p_i) = x (i, p_i) := by intros; rfl have h_eval_eq_pm' : ∀ (x y i m_i), eq_pm (x, y) (i, Sum.inr m_i) = y (i, m_i) := by intros; rfl simp_rw [h_eval_eq_pm, h_eval_eq_pm'] clear h_eval_eq_pm h_eval_eq_pm' - have h_measurable_box : Measurable fun (a : (Fin n × Fin 3 → ℝ)) => ∃ x_1 x_2, V ^ (3⁻¹:ℝ) / 2 < |a (x_1, x_2)| := by simp_rw [← Classical.not_forall_not, not_not, not_lt, abs_le] @@ -88,7 +94,6 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : apply Measurable.forall intro j refine Measurable.comp (measurableSet_setOf.mp measurableSet_Icc) (measurable_pi_apply (i, j)) - have h_measurability : Measurable fun x : (Fin n × Fin 3 → ℝ) × (Fin n × Fin 3 → ℝ) => if ∃ x_1 x_2, V ^ (3⁻¹:ℝ) / 2 < |x.1 (x_1, x_2)| then 0 else Real.exp (-(β * ∑ x_1 : Fin n × Fin 3, x.2 (x_1.1, x_1.2) ^ 2 / 2)) := by @@ -97,7 +102,6 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : convert Measurable.comp h_measurable_box measurable_fst · fun_prop · fun_prop - rw [MeasureTheory.integral_eq_lintegral_of_nonneg_ae] rotate_left · apply Filter.Eventually.of_forall @@ -108,7 +112,6 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : rw [MeasureTheory.lintegral_prod]; swap · exact (Measurable.comp (g := ENNReal.ofReal) ENNReal.measurable_ofReal h_measurability).aemeasurable - conv => enter [1, 1, 2, x, 2, y] rw [← ite_not _ _ (0:ℝ), ← boole_mul _ (Real.exp _)] @@ -118,8 +121,6 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : enter [1, 1, 2, x] simp only [not_exists, not_lt, Prod.mk.eta] rw [MeasureTheory.lintegral_const_mul' _ _ (ENNReal.ofReal_ne_top)] - - rw [MeasureTheory.lintegral_mul_const, ENNReal.toReal_mul] rw [← MeasureTheory.integral_eq_lintegral_of_nonneg_ae] rw [← MeasureTheory.integral_eq_lintegral_of_nonneg_ae] @@ -144,7 +145,6 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : fun_prop · fun_prop · fun_prop - congr 1 · --Volume of the box have h_integrand_prod : ∀ (a : Fin n × Fin 3 → ℝ), @@ -174,12 +174,14 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : simp · --Gaussian integral have h_gaussian := - GaussianFourier.integral_rexp_neg_mul_sq_norm (V := PiLp 2 (fun (_ : Fin n × Fin 3) ↦ ℝ)) (half_pos hβ) + GaussianFourier.integral_rexp_neg_mul_sq_norm + (V := PiLp 2 (fun (_ : Fin n × Fin 3) ↦ ℝ)) (half_pos hβ) apply (Eq.trans ?_ h_gaussian).trans ?_ · have := EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp (Fin n × Fin 3) rw [← this.integral_comp (MeasurableEquiv.measurableEmbedding _)] congr! 3 with x - simp_rw [div_eq_inv_mul, ← Finset.mul_sum, ← mul_assoc, neg_mul, mul_comm, PiLp.norm_sq_eq_of_L2] + simp_rw [div_eq_inv_mul, ← Finset.mul_sum, ← mul_assoc, neg_mul, mul_comm, + PiLp.norm_sq_eq_of_L2] congr! 3 simp only [Real.norm_eq_abs, sq_abs] congr @@ -189,42 +191,43 @@ theorem PartitionZ_eq (hV : 0 < V) (hβ : 0 < β) : ring_nf /-- The Helmholtz Free Energy A for an ideal gas. -/ -theorem HelmholtzA_eq (hV : 0 < V) (hT : 0 < T) : IdealGas.HelmholtzA (n,V) T = +lemma helmholtzA_eq (hV : 0 < V) (hT : 0 < T) : IdealGas.helmholtzA (n,V) T = -n * T * (Real.log V + (3/2) * Real.log (2 * Real.pi * T)) := by - rw [HelmholtzA, PartitionZT, PartitionZ_eq n hV (one_div_pos.mpr hT), Real.log_mul, + rw [helmholtzA, partitionZT, partitionZ_eq n hV (one_div_pos.mpr hT), Real.log_mul, Real.log_pow, Real.log_rpow, one_div, div_inv_eq_mul] ring_nf all_goals positivity -theorem ZIntegrable (hV : 0 < V) (hβ : 0 < β) : IdealGas.ZIntegrable (n,V) β := by - have hZpos : 0 < PartitionZ IdealGas (n, V) β := by - rw [PartitionZ_eq n hV hβ] +lemma ZIntegrable (hV : 0 < V) (hβ : 0 < β) : IdealGas.ZIntegrable (n,V) β := by + have hZpos : 0 < partitionZ IdealGas (n, V) β := by + rw [partitionZ_eq n hV hβ] positivity constructor · apply MeasureTheory.Integrable.of_integral_ne_zero - rw [← PartitionZ] + rw [← partitionZ] exact hZpos.ne' · exact hZpos.ne' /-- The ideal gas law: PV = nRT. In our unitsless system, R = 1.-/ -theorem IdealGasLaw (hV : 0 < V) (hT : 0 < T) : - let P := IdealGas.Pressure (n,V) T; +theorem ideal_gas_law (hV : 0 < V) (hT : 0 < T) : + let P := IdealGas.pressure (n,V) T; let R := 1; P * V = n * R * T := by - dsimp [Pressure] + dsimp [pressure] rw [← derivWithin_of_isOpen (s := Set.Ioi 0) isOpen_Ioi hV] - rw [derivWithin_congr (f := fun V' ↦ -n * T * (Real.log V' + (3/2) * Real.log (2 * Real.pi * T))) ?_ ?_] + rw [derivWithin_congr (f := fun V' ↦ -n * T * + (Real.log V' + (3/2) * Real.log (2 * Real.pi * T))) ?_ ?_] rw [derivWithin_of_isOpen (s := Set.Ioi 0) isOpen_Ioi hV] erw [deriv_mul (by fun_prop) (by fun_prop (disch := exact hV.ne'))] simp [field] ring_nf · intro _ hV' dsimp - rw [HelmholtzA_eq n hV' hT] + rw [helmholtzA_eq n hV' hT] ring_nf - · exact HelmholtzA_eq n hV hT + · exact helmholtzA_eq n hV hT --- 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. +-- 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 diff --git a/QuantumInfo/StatMech/ThermoQuantities.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean similarity index 64% rename from QuantumInfo/StatMech/ThermoQuantities.lean rename to Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean index e8e3a70fe..8e2d14f92 100644 --- a/QuantumInfo/StatMech/ThermoQuantities.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean @@ -5,16 +5,15 @@ Authors: Alex Meiburg -/ module -public import QuantumInfo.StatMech.Hamiltonian public import Mathlib.Analysis.SpecialFunctions.Log.Deriv -public import Mathlib.Data.Real.StarOrdered -public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.MeasureTheory.Integral.Bochner.Basic -public import Mathlib.MeasureTheory.Integral.Bochner.L1 -public import Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory public import Mathlib.MeasureTheory.Measure.Haar.OfBasis -public import Mathlib.Order.CompletePartialOrder +public import Physlib.StatisticalMechanics.MicroCanonicalEnsemble.Basic +/-! +## The theormodynamical quantities of a microcanonical ensemble + +-/ @[expose] public section noncomputable section @@ -22,48 +21,51 @@ namespace MicroHamiltonian variable {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. +/-- 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 + * Ideally this would be an NNReal, but ∫ (NNReal) doesn't work right now, so it would just be a + separate proof anyway -/ -def PartitionZ (β : ℝ) : ℝ := +def partitionZ (β : ℝ) : ℝ := ∫ (config : H.dim d → ℝ), let E := H.H config if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h)) /-- The partition function as a function of temperature T instead of β. -/ -def PartitionZT (T : ℝ) : ℝ := - PartitionZ H d (1/T) +def partitionZT (T : ℝ) : ℝ := + partitionZ H d (1/T) /-- The Internal Energy, U or E, defined as -∂(ln Z)/∂β. Parameterized here with β. -/ -def InternalU (β : ℝ) : ℝ := - -deriv (fun β' ↦ (PartitionZ H d β').log) β +def internalU (β : ℝ) : ℝ := + -deriv (fun β' ↦ (partitionZ H d β').log) β -/-- The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not β. -/ -def HelmholtzA (T : ℝ) : ℝ := - -T * (PartitionZT H d T).log +/-- The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not + β. -/ +def helmholtzA (T : ℝ) : ℝ := + -T * (partitionZT H d T).log /-- The entropy, defined as the -∂A/∂T. Function of T. -/ -def EntropyS (T : ℝ) : ℝ := - -deriv (HelmholtzA H d) T +def entropyS (T : ℝ) : ℝ := + -deriv (helmholtzA H d) T /-- The entropy, defined as ln Z + β*U. Function of β. -/ -def EntropySβ (β : ℝ) : ℝ := - (PartitionZ H d β).log + β * InternalU H d β +def entropySβ (β : ℝ) : ℝ := + (partitionZ H d β).log + β * internalU H d β -/-- 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. +/-- 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. -/ def ZIntegrable (β : ℝ) : Prop := MeasureTheory.Integrable (fun (config : H.dim d → ℝ) ↦ let E := H.H config; if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h)) - ) ∧ (H.PartitionZ d β ≠ 0) + ) ∧ (H.partitionZ d β ≠ 0) /-- -This Prop defines the most common case of ZIntegrable, that it is integrable at all finite temperatures -(aka all positive β). +This Prop defines the most common case of ZIntegrable, that it is integrable at all finite +temperatures (aka all positive β). -/ def PositiveβIntegrable : Prop := ∀ β > 0, H.ZIntegrable d β @@ -84,28 +86,30 @@ so this will be differentiable if ∫ exp(-βE) * μ⁻(H,E) dE is, aka if the Laplace transform is differentiable. See e.g. https://math.stackexchange.com/q/84382/127777 -For this we really want the fact that the Laplace transform is analytic wherever it's absolutely convergent, -which is (as Wikipedia informs) an easy consequence of Fubini's theorem + Morera's theorem. However, Morera's -theorem isn't in mathlib yet. So this is a sorry for now +For this we really want the fact that the Laplace transform is analytic wherever it's absolutely +convergent, which is (as Wikipedia informs) an easy consequence of Fubini's theorem + Morera's +theorem. However, Morera's theorem isn't in mathlib yet. So this is a sorry for now -/ open scoped ContDiff in -theorem DifferentiableAt_Z_if_ZIntegrable {β : ℝ} (h : H.ZIntegrable d β) : ContDiffAt ℝ ω (H.PartitionZ d) β := - sorry +@[sorryful] +lemma differentiableAt_Z_if_ZIntegrable {β : ℝ} (h : H.ZIntegrable d β) : + ContDiffAt ℝ ω (H.partitionZ d) β := sorry /-- The two definitions of entropy, in terms of T or β, are equivalent. -/ -theorem entropy_A_eq_entropy_Z (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegrable d β) - : EntropyS H d T = EntropySβ H d β := by +@[sorryful] +lemma entropy_A_eq_entropy_Z (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegrable d β) : + entropyS H d T = entropySβ H d β := by have hTnz : T ≠ 0 := left_ne_zero_of_mul_eq_one hβT have hβnz : β ≠ 0 := right_ne_zero_of_mul_eq_one hβT have hβT' := eq_one_div_of_mul_eq_one_right hβT - dsimp [EntropyS, EntropySβ, InternalU, PartitionZT] - unfold HelmholtzA + dsimp [entropyS, entropySβ, internalU, partitionZT] + unfold helmholtzA erw [deriv_mul] rw [deriv_neg'', neg_mul, one_mul, neg_add_rev, neg_neg, mul_neg, add_comm] congr 1 - · rw [PartitionZT, hβT'] - simp_rw [PartitionZT] - have hdc := deriv_comp (h := fun T ↦ T⁻¹) (h₂ := fun β => Real.log (H.PartitionZ d β)) T ?_ ?_ + · rw [partitionZT, hβT'] + simp_rw [partitionZT] + have hdc := deriv_comp (h := fun T ↦ T⁻¹) (h₂ := fun β => Real.log (H.partitionZ d β)) T ?_ ?_ unfold Function.comp at hdc simp only [hdc, one_div, deriv_inv', mul_neg, neg_inj, hβT'] field_simp @@ -113,14 +117,14 @@ theorem entropy_A_eq_entropy_Z (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegra --Show the differentiability side-goals · rw [← one_div, ← hβT'] have h₁ := hi.2 - have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero + have := (differentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero fun_prop (disch := assumption) · fun_prop (disch := assumption) · fun_prop - · simp_rw [PartitionZT] + · simp_rw [partitionZT] rw [hβT'] at hi have := hi.2 - have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero + have := (differentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero fun_prop (disch := assumption) set_option backward.isDefEq.respectTransparency false in @@ -130,29 +134,29 @@ The "definition of temperature from entropy": 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 β. -/ -theorem β_eq_deriv_S_U {β : ℝ} (hi : H.ZIntegrable d β) : β = (deriv (H.EntropySβ d) β) / deriv (H.InternalU d) β := by - unfold EntropySβ - unfold InternalU - +@[sorryful] +lemma β_eq_deriv_S_U {β : ℝ} (hi : H.ZIntegrable d β) : + β = (deriv (H.entropySβ d) β) / deriv (H.internalU d) β := by + unfold entropySβ + unfold internalU --Show the differentiability side-goals - have : DifferentiableAt ℝ (fun β => Real.log (H.PartitionZ d β)) β := by + have : DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) β := by have := hi.2 - have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero + have := (differentiableAt_Z_if_ZIntegrable hi).differentiableAt WithTop.top_ne_zero fun_prop (disch := assumption) - have : DifferentiableAt ℝ (deriv fun β => Real.log (H.PartitionZ d β)) β := by - have this := (DifferentiableAt_Z_if_ZIntegrable hi).log hi.2 + have : DifferentiableAt ℝ (deriv fun β => Real.log (H.partitionZ d β)) β := by + have this := (differentiableAt_Z_if_ZIntegrable hi).log hi.2 replace this := (this.fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt WithTop.top_ne_zero unfold deriv fun_prop - --Main goal simp only [mul_neg] erw [deriv.neg', deriv_add, deriv.neg'] dsimp erw [deriv_mul] simp only [deriv_id'', one_mul, neg_add_rev, add_neg_cancel_comm_assoc, neg_div_neg_eq] - have : deriv (deriv fun β => Real.log (H.PartitionZ d β)) β ≠ 0 := ?_ + have : deriv (deriv fun β => Real.log (H.partitionZ d β)) β ≠ 0 := ?_ exact (mul_div_cancel_right₀ β this).symm --Discharge those side-goals · sorry @@ -178,8 +182,8 @@ open MicroHamiltonian variable (H : NVEHamiltonian) (d : ℕ × ℝ) /-- Pressure, as a function of T. Defined as the conjugate variable to volume. -/ -def Pressure (T : ℝ) : ℝ := +def pressure (T : ℝ) : ℝ := let (n, V) := d; - -deriv (fun V' ↦ HelmholtzA H (n, V') T) V + - deriv (fun V' ↦ helmholtzA H (n, V') T) V end NVEHamiltonian diff --git a/QuantumInfo.lean b/QuantumInfo.lean index ad8920976..f9c6fd216 100644 --- a/QuantumInfo.lean +++ b/QuantumInfo.lean @@ -37,8 +37,3 @@ public import QuantumInfo.Finite.Capacity_doc public import QuantumInfo.ClassicalInfo.Distribution public import QuantumInfo.ClassicalInfo.Entropy public import QuantumInfo.ClassicalInfo.Prob - ---Statistical mechanics -public import QuantumInfo.StatMech.Hamiltonian -public import QuantumInfo.StatMech.IdealGas -public import QuantumInfo.StatMech.ThermoQuantities diff --git a/QuantumInfo/StatMech/Hamiltonian.lean b/QuantumInfo/StatMech/Hamiltonian.lean deleted file mode 100644 index 28213a86f..000000000 --- a/QuantumInfo/StatMech/Hamiltonian.lean +++ /dev/null @@ -1,42 +0,0 @@ -/- -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 Mathlib.Data.Fintype.Defs -public import Mathlib.Data.Real.Basic - -@[expose] public section - -section ThermodynamicEnsemble - -/-- The Hamiltonian for a microcanonical ensemble, parameterized by any extrinsic parameters of data D. - Since it's an arbitrary type, 'T' would be nice, but we use 'D' for data to avoid confusion with temperature. - We define Hamiltonians as an energy function on a real manifold, whose dimension n possibly depends on the data D. - Energy is a WithTop ℝ, ⊤ is used to mean "excluded as a possibility in phase space". - This formalization does exclude the possibility of discrete degrees of freedom; it is not _completely_ general. - A better formalization could have an arbitrary measurable space. --/ -structure MicroHamiltonian (D : Type) where - --For extrinsic parameters D (e.g. the number of particles of different chemical species, the shape of the box), - --how many continuous degrees of freedom are there? - dim : D → Type - --We require that the number of degrees of freedom is finite. - [dim_fin : ∀ d, Fintype (dim d)] - --Given the configuration, what is its energy? - H : {d : D} → (dim d → ℝ) → WithTop ℝ - -/-- We add the dim_fin to the instance cache so that things like the measure can be synthesized -/ -instance microHamiltonianFintype (H : MicroHamiltonian D) (d : D) : Fintype (H.dim d) := - H.dim_fin d - -/-- The standard microcanonical ensemble Hamiltonian, where the data is the particle number N and the volume V. -/ -abbrev NVEHamiltonian := MicroHamiltonian (ℕ × ℝ) - -/-- Helper to get the number in an N-V Hamiltonian -/ -def NVEHamiltonian.N : (ℕ × ℝ) → ℕ := Prod.fst - -/-- Helper to get the volume in an N-V Hamiltonian -/ -def NVEHamiltonian.V : (ℕ × ℝ) → ℝ := Prod.snd diff --git a/scripts/lint_all.lean b/scripts/lint_all.lean index 1bbc84ec5..47ec83fbd 100644 --- a/scripts/lint_all.lean +++ b/scripts/lint_all.lean @@ -31,6 +31,7 @@ def main (args : List String) : IO UInt32 := do println! "\x1b[36m(5/7) Sorry and pseudo attribute linter \x1b[0m" let sorryPseudoCheck ← IO.Process.output {cmd := "lake", args := #["exe", "sorry_lint"]} println! sorryPseudoCheck.stdout + println! sorryPseudoCheck.stderr if ¬ "--fast" ∈ args then println! "\x1b[36m(6/7) Lean linter \x1b[0m" From f45e47807a37cc504629a1d53907dcd434b15243 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 6 May 2026 11:47:28 +0100 Subject: [PATCH 2/4] refactor: Lint --- .../MicroCanonicalEnsemble/IdealGas.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean index a73e8f96a..3e4f4560d 100644 --- a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/IdealGas.lean @@ -166,7 +166,9 @@ lemma partitionZ_eq (hV : 0 < V) (hβ : 0 < β) : (measurableSet_Icc (a := -(V ^ (3⁻¹ : ℝ) / 2)) (b := (V ^ (3⁻¹ : ℝ) / 2))) simp_rw [Set.indicator] at h_indicator simp_rw [abs_le, ← Set.mem_Icc, h_indicator] - simp + simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter, + Real.volume_real_Icc, sub_neg_eq_add, add_halves, smul_eq_mul, mul_one, sup_eq_left, + ge_iff_le] positivity rw [h_integral_1d]; clear h_integral_1d rw [← Real.rpow_mul_natCast hV.le] @@ -187,7 +189,8 @@ lemma partitionZ_eq (hV : 0 < V) (hβ : 0 < β) : congr · field_simp congr - simp + simp only [finrank_euclideanSpace, Fintype.card_prod, Fintype.card_fin, Nat.cast_mul, + Nat.cast_ofNat] ring_nf /-- The Helmholtz Free Energy A for an ideal gas. -/ From 0e03f97d7219d76820b05c5dbad0fae3dcb00e9f Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 8 May 2026 13:18:36 -0400 Subject: [PATCH 3/4] Apply suggestion from @Timeroot --- .../MicroCanonicalEnsemble/ThermoQuantities.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean index 8e2d14f92..a80918fae 100644 --- a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean @@ -88,7 +88,9 @@ is, aka if the Laplace transform is differentiable. See e.g. https://math.stackexchange.com/q/84382/127777 For this we really want the fact that the Laplace transform is analytic wherever it's absolutely convergent, which is (as Wikipedia informs) an easy consequence of Fubini's theorem + Morera's -theorem. However, Morera's theorem isn't in mathlib yet. So this is a sorry for now +theorem. Morera's theorem is now in Mathlib as `Complex.IsConservativeOn.isExactOn_ball` (in HasPrimitives.lean), so this would be a good task: + - Prove the analyticity of the Laplace transform + - Use this to show that the partition function Z here is analytic (ContDiffAt ℝ ω) -/ open scoped ContDiff in @[sorryful] From 708aa765fb1919d475b3319630a3844dd56431ec Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 8 May 2026 13:20:32 -0400 Subject: [PATCH 4/4] fix long line --- .../MicroCanonicalEnsemble/ThermoQuantities.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean index a80918fae..2afca2de4 100644 --- a/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean +++ b/Physlib/StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities.lean @@ -88,7 +88,8 @@ is, aka if the Laplace transform is differentiable. See e.g. https://math.stackexchange.com/q/84382/127777 For this we really want the fact that the Laplace transform is analytic wherever it's absolutely convergent, which is (as Wikipedia informs) an easy consequence of Fubini's theorem + Morera's -theorem. Morera's theorem is now in Mathlib as `Complex.IsConservativeOn.isExactOn_ball` (in HasPrimitives.lean), so this would be a good task: +theorem. Morera's theorem is now in Mathlib as `Complex.IsConservativeOn.isExactOn_ball` (in +HasPrimitives.lean), so this would be a good task: - Prove the analyticity of the Laplace transform - Use this to show that the partition function Z here is analytic (ContDiffAt ℝ ω) -/