IndisputableMonolith.Cosmology.StatisticsKernels
IndisputableMonolith/Cosmology/StatisticsKernels.lean · 387 lines · 31 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.PhaseSpaceReduction
3
4/-!
5# Statistics Kernels: `∓ln(1∓e^{−t})` and `t/(eᵗ∓1)` from the partition function
6
7## What this module derives
8
9`PhaseSpaceReduction` (and `GrandPotential` before it) took the Bose/Fermi
10pressure kernels `−ln(1−e^{−t})`, `ln(1+e^{−t})` and energy kernels
11`t/(eᵗ∓1)` as *definitions* (MODEL). This module derives all four from
12the grand partition function of a single mode at `μ = 0`:
13
14 `Z_mode = Σ_n e^{−n·E/T}` over the allowed occupancies `n`,
15
16with `t = E/T` dimensionless. The only inputs are:
17
18* the Gibbs weight `e^{−n·t}` of the `n`-quanta microstate, and
19* the occupancy sets: `n ∈ ℕ` for bosons (unrestricted),
20 `n ∈ {0, 1}` for fermions (Pauli exclusion).
21
22From these:
23
241. **Partition functions** (`bosePartition_eq`, `fermiPartition_eq`):
25 the geometric series gives `Z_B = (1−e^{−t})⁻¹`; the two-state sum
26 gives `Z_F = 1 + e^{−t}`.
272. **Pressure kernels are `ln Z`** (`boseLogKernel_eq_log_partition`,
28 `fermiLogKernel_eq_log_partition`): the previously-defined log kernels
29 are literally `ln Z_mode`.
303. **Occupation numbers** (`boseOccupation_eq`, `fermiOccupation_eq`):
31 the ensemble mean `⟨n⟩ = (Σ n·wₙ)/Z` evaluates to the Bose–Einstein
32 `1/(eᵗ−1)` and Fermi–Dirac `1/(eᵗ+1)` distributions.
334. **Energy kernels are `t·⟨n⟩`** (`boseEnergyKernel_eq_occupation`,
34 `fermiEnergyKernel_eq_occupation`).
355. **Thermodynamic consistency** (`boseLogKernel_hasDerivAt`,
36 `mode_energy_bose`, …): `⟨n⟩ = −d(ln Z)/dt`, and in physical
37 variables `⟨E⟩ = −∂_β ln Z` per mode — the pressure and energy
38 kernels are not independent inputs but derivative-related, exactly
39 as the grand-canonical formalism demands.
406. **Capstones** (`plasmaPressure_from_partitionFunction`,
41 `plasmaEnergy_from_occupation`): the plasma pressure/energy of the
42 η_B chain now start from `Σ e^{−nE/T}` in momentum space.
43
44## Provenance ledger (honest tags)
45
46* THEOREM (this module): the four kernel functional forms; the BE/FD
47 distributions; `⟨n⟩ = −d ln Z/dt`; `⟨E⟩ = −∂_β ln Z`; the Pauli bound
48 `⟨n⟩_F < 1`; the identification with the `GrandPotential` integrands.
49* MODEL (remaining upstream inputs): the Gibbs weight `e^{−βE}` itself
50 (the canonical-ensemble measure), and the occupancy sets — bosonic
51 `ℕ` vs fermionic `{0,1}`. The RS-side exclusion principle is
52 formalized as a J-cost statement in
53 `Foundation.PauliExclusionFromJCost` / `Foundation.SpinStatistics`;
54 the bridge from that certificate to the occupancy set `{0,1}` used
55 here remains OPEN.
56-/
57
58namespace IndisputableMonolith
59namespace Cosmology
60namespace StatisticsKernels
61
62open Real MeasureTheory Set
63open PhaseSpaceReduction (boseLogKernel fermiLogKernel boseEnergyKernel
64 fermiEnergyKernel phaseSpaceDensity)
65
66/-! ## §1. Single-mode Gibbs weights and partition functions -/
67
68/-- Gibbs weight of the `n`-quanta microstate of a mode at dimensionless
69energy `t = E/T` (equivalently `β·E`), chemical potential zero:
70`w_n = e^{−n·t}`. -/
71noncomputable def boltzmannWeight (t : ℝ) (n : ℕ) : ℝ := Real.exp (-(n * t))
72
73/-- Bosonic single-mode grand partition function: unrestricted occupancy,
74`Z_B(t) = Σ_{n∈ℕ} e^{−n·t}`. -/
75noncomputable def bosePartition (t : ℝ) : ℝ := ∑' n : ℕ, boltzmannWeight t n
76
77/-- Fermionic single-mode grand partition function: Pauli-restricted
78occupancy `n ∈ {0,1}`, `Z_F(t) = Σ_{n<2} e^{−n·t}`. -/
79noncomputable def fermiPartition (t : ℝ) : ℝ :=
80 ∑ n ∈ Finset.range 2, boltzmannWeight t n
81
82/-- Mean occupation of a bosonic mode: `⟨n⟩ = (Σ n·w_n)/Z_B`. -/
83noncomputable def boseOccupation (t : ℝ) : ℝ :=
84 (∑' n : ℕ, (n : ℝ) * boltzmannWeight t n) / bosePartition t
85
86/-- Mean occupation of a fermionic mode: `⟨n⟩ = (Σ_{n<2} n·w_n)/Z_F`. -/
87noncomputable def fermiOccupation (t : ℝ) : ℝ :=
88 (∑ n ∈ Finset.range 2, (n : ℝ) * boltzmannWeight t n) / fermiPartition t
89
90/-- The Gibbs weight is the `n`-th power of the one-quantum weight. -/
91lemma boltzmannWeight_pow (t : ℝ) (n : ℕ) :
92 boltzmannWeight t n = Real.exp (-t) ^ n := by
93 unfold boltzmannWeight
94 rw [← Real.exp_nat_mul]
95 ring_nf
96
97lemma exp_neg_lt_one {t : ℝ} (ht : 0 < t) : Real.exp (-t) < 1 :=
98 Real.exp_lt_one_iff.mpr (by linarith)
99
100lemma one_lt_exp {t : ℝ} (ht : 0 < t) : 1 < Real.exp t := by
101 rw [← Real.exp_zero]
102 exact Real.exp_lt_exp.mpr ht
103
104/-! ## §2. Closed forms of the partition functions -/
105
106/-- **Bose partition function** (geometric series): for `t > 0`,
107`Z_B(t) = (1 − e^{−t})⁻¹`. -/
108theorem bosePartition_eq {t : ℝ} (ht : 0 < t) :
109 bosePartition t = (1 - Real.exp (-t))⁻¹ := by
110 unfold bosePartition
111 simp only [boltzmannWeight_pow]
112 exact tsum_geometric_of_lt_one (le_of_lt (Real.exp_pos _))
113 (exp_neg_lt_one ht)
114
115/-- **Fermi partition function** (two occupancy states):
116`Z_F(t) = 1 + e^{−t}`, for every `t`. -/
117theorem fermiPartition_eq (t : ℝ) :
118 fermiPartition t = 1 + Real.exp (-t) := by
119 unfold fermiPartition boltzmannWeight
120 simp [Finset.sum_range_succ]
121
122lemma bosePartition_pos {t : ℝ} (ht : 0 < t) : 0 < bosePartition t := by
123 rw [bosePartition_eq ht]
124 have := exp_neg_lt_one ht
125 exact inv_pos.mpr (by linarith)
126
127lemma fermiPartition_pos (t : ℝ) : 0 < fermiPartition t := by
128 rw [fermiPartition_eq]
129 positivity
130
131/-! ## §3. The pressure kernels are `ln Z_mode` -/
132
133/-- **THEOREM: the Bose pressure kernel is the log partition function.**
134`−ln(1−e^{−t}) = ln Z_B(t)`. The kernel that was a definition in
135`PhaseSpaceReduction` is the grand-canonical `ln Z` of one mode. -/
136theorem boseLogKernel_eq_log_partition {t : ℝ} (ht : 0 < t) :
137 boseLogKernel t = Real.log (bosePartition t) := by
138 rw [bosePartition_eq ht, Real.log_inv]
139 rfl
140
141/-- **THEOREM: the Fermi pressure kernel is the log partition function.**
142`ln(1+e^{−t}) = ln Z_F(t)`. -/
143theorem fermiLogKernel_eq_log_partition (t : ℝ) :
144 fermiLogKernel t = Real.log (fermiPartition t) := by
145 rw [fermiPartition_eq]
146 rfl
147
148/-! ## §4. The occupation numbers: Bose–Einstein and Fermi–Dirac -/
149
150/-- **THEOREM (Bose–Einstein distribution).** The ensemble-mean
151occupation of a bosonic mode is `⟨n⟩_B = 1/(eᵗ−1)`: the weighted
152geometric series `Σ n·xⁿ = x/(1−x)²` divided by `Z_B = (1−x)⁻¹`. -/
153theorem boseOccupation_eq {t : ℝ} (ht : 0 < t) :
154 boseOccupation t = 1 / (Real.exp t - 1) := by
155 unfold boseOccupation
156 rw [bosePartition_eq ht]
157 simp only [boltzmannWeight_pow]
158 have hx0 : (0 : ℝ) ≤ Real.exp (-t) := le_of_lt (Real.exp_pos _)
159 have hx1 : Real.exp (-t) < 1 := exp_neg_lt_one ht
160 rw [tsum_coe_mul_geometric_of_norm_lt_one
161 (by rw [Real.norm_of_nonneg hx0]; exact hx1)]
162 have hy : 1 < Real.exp t := one_lt_exp ht
163 have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
164 have hy1 : Real.exp t - 1 ≠ 0 := by linarith
165 have h1x : 1 - Real.exp (-t) ≠ 0 := by linarith
166 rw [Real.exp_neg]
167 rw [Real.exp_neg] at h1x
168 field_simp
169
170/-- **THEOREM (Fermi–Dirac distribution).** The ensemble-mean occupation
171of a fermionic mode is `⟨n⟩_F = 1/(eᵗ+1)`, for every `t` (the two-state
172sum needs no convergence condition). -/
173theorem fermiOccupation_eq (t : ℝ) :
174 fermiOccupation t = 1 / (Real.exp t + 1) := by
175 unfold fermiOccupation boltzmannWeight
176 rw [fermiPartition_eq]
177 simp only [Finset.sum_range_succ, Finset.sum_range_zero,
178 Nat.cast_zero, Nat.cast_one, zero_mul, one_mul, neg_zero,
179 Real.exp_zero, zero_add, add_zero]
180 have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
181 have hpos : (0 : ℝ) < 1 + Real.exp (-t) := by positivity
182 rw [Real.exp_neg]
183 rw [Real.exp_neg] at hpos
184 field_simp
185
186/-- **Pauli bound.** A fermionic mode is never more than singly
187occupied on average: `⟨n⟩_F < 1`. This is the statistical shadow of the
188occupancy restriction `n ∈ {0,1}`. -/
189theorem fermiOccupation_lt_one (t : ℝ) : fermiOccupation t < 1 := by
190 rw [fermiOccupation_eq]
191 have h := Real.exp_pos t
192 rw [div_lt_one (by linarith)]
193 linarith
194
195/-- A bosonic mode at positive energy has positive mean occupation. -/
196theorem boseOccupation_pos {t : ℝ} (ht : 0 < t) : 0 < boseOccupation t := by
197 rw [boseOccupation_eq ht]
198 have := one_lt_exp ht
199 exact div_pos one_pos (by linarith)
200
201/-! ## §5. The energy kernels are `t·⟨n⟩` -/
202
203/-- **THEOREM: the Bose energy kernel is `t·⟨n⟩_B`.** The integrand of
204the plasma energy is (dimensionless energy) × (mean occupation). -/
205theorem boseEnergyKernel_eq_occupation {t : ℝ} (ht : 0 < t) :
206 boseEnergyKernel t = t * boseOccupation t := by
207 rw [boseOccupation_eq ht]
208 unfold PhaseSpaceReduction.boseEnergyKernel
209 ring
210
211/-- **THEOREM: the Fermi energy kernel is `t·⟨n⟩_F`.** -/
212theorem fermiEnergyKernel_eq_occupation (t : ℝ) :
213 fermiEnergyKernel t = t * fermiOccupation t := by
214 rw [fermiOccupation_eq]
215 unfold PhaseSpaceReduction.fermiEnergyKernel
216 ring
217
218/-! ## §6. Thermodynamic consistency: `⟨n⟩ = −d(ln Z)/dt` -/
219
220/-- **THEOREM (grand-canonical consistency, Bose).** The mean occupation
221is minus the derivative of the log partition function with respect to the
222dimensionless energy: `d/dt[−ln(1−e^{−t})] = −⟨n⟩_B(t)`. The pressure
223and energy kernels are therefore *one* input, not two. -/
224theorem boseLogKernel_hasDerivAt {t : ℝ} (ht : 0 < t) :
225 HasDerivAt boseLogKernel (-(boseOccupation t)) t := by
226 have h1 : HasDerivAt (fun s : ℝ => -s) (-1) t := (hasDerivAt_id t).neg
227 have h2 : HasDerivAt (fun s : ℝ => Real.exp (-s))
228 (Real.exp (-t) * (-1)) t := (Real.hasDerivAt_exp (-t)).comp t h1
229 have h3 : HasDerivAt (fun s : ℝ => 1 - Real.exp (-s))
230 (0 - Real.exp (-t) * (-1)) t := (hasDerivAt_const t 1).sub h2
231 have hlt : Real.exp (-t) < 1 := exp_neg_lt_one ht
232 have hne : 1 - Real.exp (-t) ≠ 0 := by linarith
233 have h4 := (h3.log hne).neg
234 have heq : -((0 - Real.exp (-t) * (-1)) / (1 - Real.exp (-t)))
235 = -(boseOccupation t) := by
236 rw [boseOccupation_eq ht]
237 have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
238 have hy1 : Real.exp t - 1 ≠ 0 := by
239 have := one_lt_exp ht; linarith
240 rw [Real.exp_neg]
241 rw [Real.exp_neg] at hne
242 field_simp
243 ring
244 rw [← heq]
245 exact h4
246
247/-- **THEOREM (grand-canonical consistency, Fermi).**
248`d/dt[ln(1+e^{−t})] = −⟨n⟩_F(t)`, for every `t`. -/
249theorem fermiLogKernel_hasDerivAt (t : ℝ) :
250 HasDerivAt fermiLogKernel (-(fermiOccupation t)) t := by
251 have h1 : HasDerivAt (fun s : ℝ => -s) (-1) t := (hasDerivAt_id t).neg
252 have h2 : HasDerivAt (fun s : ℝ => Real.exp (-s))
253 (Real.exp (-t) * (-1)) t := (Real.hasDerivAt_exp (-t)).comp t h1
254 have h3 : HasDerivAt (fun s : ℝ => 1 + Real.exp (-s))
255 (0 + Real.exp (-t) * (-1)) t := (hasDerivAt_const t 1).add h2
256 have hpos : (0 : ℝ) < 1 + Real.exp (-t) := by positivity
257 have h4 := h3.log (ne_of_gt hpos)
258 have heq : (0 + Real.exp (-t) * (-1)) / (1 + Real.exp (-t))
259 = -(fermiOccupation t) := by
260 rw [fermiOccupation_eq]
261 have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
262 rw [Real.exp_neg]
263 rw [Real.exp_neg] at hpos
264 field_simp
265 ring
266 rw [← heq]
267 exact h4
268
269/-- The energy kernel is `−t` times the derivative of the pressure
270kernel: `t/(eᵗ−1) = −t·(d/dt) ln Z_B`. Pressure kernel in, energy kernel
271out — no independent input. -/
272theorem boseEnergyKernel_from_logKernel {t : ℝ} (ht : 0 < t) :
273 boseEnergyKernel t = -t * deriv boseLogKernel t := by
274 rw [(boseLogKernel_hasDerivAt ht).deriv, boseEnergyKernel_eq_occupation ht]
275 ring
276
277/-- Fermi version: `t/(eᵗ+1) = −t·(d/dt) ln Z_F`. -/
278theorem fermiEnergyKernel_from_logKernel (t : ℝ) :
279 fermiEnergyKernel t = -t * deriv fermiLogKernel t := by
280 rw [(fermiLogKernel_hasDerivAt t).deriv, fermiEnergyKernel_eq_occupation]
281 ring
282
283/-! ## §7. Physical variables: `⟨E⟩ = −∂_β ln Z` per mode -/
284
285/-- **THEOREM (textbook form, Bose).** For a mode of energy `E > 0`, the
286mean energy is minus the β-derivative of the log partition function:
287`−∂_β ln Z_B(βE) = E·⟨n⟩_B(βE)`. -/
288theorem mode_energy_bose (E : ℝ) (hE : 0 < E) {β : ℝ} (hβ : 0 < β) :
289 HasDerivAt (fun b => Real.log (bosePartition (b * E)))
290 (-(E * boseOccupation (β * E))) β := by
291 have h1 : HasDerivAt (fun b : ℝ => b * E) E β := by
292 simpa using (hasDerivAt_id β).mul_const E
293 have hβE : 0 < β * E := mul_pos hβ hE
294 have h2 := (boseLogKernel_hasDerivAt hβE).comp β h1
295 have h3 : HasDerivAt (fun b => boseLogKernel (b * E))
296 (-(E * boseOccupation (β * E))) β := by
297 convert h2 using 1
298 ring
299 apply h3.congr_of_eventuallyEq
300 filter_upwards [Ioi_mem_nhds hβ] with b hb
301 exact (boseLogKernel_eq_log_partition (mul_pos hb hE)).symm
302
303/-- **THEOREM (textbook form, Fermi).** `−∂_β ln Z_F(βE) = E·⟨n⟩_F(βE)`. -/
304theorem mode_energy_fermi (E : ℝ) {β : ℝ} :
305 HasDerivAt (fun b => Real.log (fermiPartition (b * E)))
306 (-(E * fermiOccupation (β * E))) β := by
307 have h1 : HasDerivAt (fun b : ℝ => b * E) E β := by
308 simpa using (hasDerivAt_id β).mul_const E
309 have h2 := (fermiLogKernel_hasDerivAt (β * E)).comp β h1
310 have h3 : HasDerivAt (fun b => fermiLogKernel (b * E))
311 (-(E * fermiOccupation (β * E))) β := by
312 convert h2 using 1
313 ring
314 apply h3.congr_of_eventuallyEq
315 filter_upwards [Filter.univ_mem] with b _
316 exact (fermiLogKernel_eq_log_partition (b * E)).symm
317
318/-! ## §8. Capstones: the plasma potential starts at `Σ e^{−nE/T}` -/
319
320/-- The bose kernels agree a.e. in momentum space (they differ at most at
321`k = 0`, a null set), so the phase-space integrals coincide. -/
322lemma phaseSpaceDensity_congr_pos (g T : ℝ) (hT : 0 < T) (K₁ K₂ : ℝ → ℝ)
323 (h : ∀ t : ℝ, 0 < t → K₁ t = K₂ t) :
324 phaseSpaceDensity 3 g T K₁ = phaseSpaceDensity 3 g T K₂ := by
325 unfold PhaseSpaceReduction.phaseSpaceDensity
326 congr 1
327 apply integral_congr_ae
328 have h0 : (volume : Measure (EuclideanSpace ℝ (Fin 3))) {0} = 0 :=
329 measure_singleton 0
330 filter_upwards [compl_mem_ae_iff.mpr h0] with k hk
331 have hknorm : (0 : ℝ) < ‖k‖ := norm_pos_iff.mpr (by simpa using hk)
332 rw [h (‖k‖ / T) (div_pos hknorm hT)]
333
334/-- **CAPSTONE (pressure).** The plasma pressure of the η_B chain equals
335the phase-space integral of `T·ln Z_mode(E/T)` — the grand-canonical
336pressure `P = (T/V)·ln Z` — with `Z_B = Σ_{n∈ℕ} e^{−nE/T}` and
337`Z_F = Σ_{n∈{0,1}} e^{−nE/T}`. The log kernels are gone as inputs; only
338the Gibbs weight and the occupancy sets remain. -/
339theorem plasmaPressure_from_partitionFunction (gB gF : ℝ) {T : ℝ}
340 (hT : 0 < T) :
341 phaseSpaceDensity 3 gB T (fun t => Real.log (bosePartition t))
342 + phaseSpaceDensity 3 gF T (fun t => Real.log (fermiPartition t))
343 = GrandPotential.plasmaPressure gB gF T := by
344 have hB := phaseSpaceDensity_congr_pos gB T hT
345 (fun t => Real.log (bosePartition t)) boseLogKernel
346 (fun t ht => (boseLogKernel_eq_log_partition ht).symm)
347 have hF := phaseSpaceDensity_congr_pos gF T hT
348 (fun t => Real.log (fermiPartition t)) fermiLogKernel
349 (fun t _ => (fermiLogKernel_eq_log_partition t).symm)
350 rw [hB, hF]
351 exact PhaseSpaceReduction.plasmaPressure_from_phaseSpace gB gF hT
352
353/-- **CAPSTONE (energy).** The plasma energy equals the phase-space
354integral of `E·⟨n⟩(E/T)`: mean occupation times mode energy, with `⟨n⟩`
355derived from the same partition functions. -/
356theorem plasmaEnergy_from_occupation (gB gF : ℝ) {T : ℝ} (hT : 0 < T) :
357 phaseSpaceDensity 3 gB T (fun t => t * boseOccupation t)
358 + phaseSpaceDensity 3 gF T (fun t => t * fermiOccupation t)
359 = GrandPotential.plasmaEnergy gB gF T := by
360 have hB := phaseSpaceDensity_congr_pos gB T hT
361 (fun t => t * boseOccupation t) boseEnergyKernel
362 (fun t ht => (boseEnergyKernel_eq_occupation ht).symm)
363 have hF := phaseSpaceDensity_congr_pos gF T hT
364 (fun t => t * fermiOccupation t) fermiEnergyKernel
365 (fun t _ => (fermiEnergyKernel_eq_occupation t).symm)
366 rw [hB, hF]
367 exact PhaseSpaceReduction.plasmaEnergy_from_phaseSpace gB gF hT
368
369/-! ## §9. The number-density integrand is `t²·⟨n⟩` -/
370
371/-- The photon/boson number integrand of `NumberDensityIntegral`
372(`t²/(eᵗ−1)`, whose integral is `2ζ(3)`) is `t²·⟨n⟩_B(t)`: number density
373counts occupation over modes. -/
374theorem number_integrand_bose {t : ℝ} (ht : 0 < t) :
375 t ^ 2 * boseOccupation t = t ^ 2 / (Real.exp t - 1) := by
376 rw [boseOccupation_eq ht]; ring
377
378/-- Fermion number integrand (`t²/(eᵗ+1)`, integral `(3/2)ζ(3)`) is
379`t²·⟨n⟩_F(t)`. -/
380theorem number_integrand_fermi (t : ℝ) :
381 t ^ 2 * fermiOccupation t = t ^ 2 / (Real.exp t + 1) := by
382 rw [fermiOccupation_eq]; ring
383
384end StatisticsKernels
385end Cosmology
386end IndisputableMonolith
387