IndisputableMonolith.Cosmology.RadiationEntropyRelation
IndisputableMonolith/Cosmology/RadiationEntropyRelation.lean · 468 lines · 29 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.FermionWeightIntegral
3import IndisputableMonolith.Cosmology.NumberDensityIntegral
4
5/-!
6# The Radiation Entropy Relation s = (4/3)·ρ/T from the Entropy Functional
7
8**Status: THEOREM (this module, 0 sorry).**
9
10This module closes the next MODEL element in the η_B chain: the
11statistical-mechanics identification `s = (4/3)·ρ/T` for a massless quantum
12gas. Up to now the entropy chain (`EntropyPerPhoton`, `NumberDensityIntegral`)
13*used* the 4/3 factor as an assumed thermodynamic input. Here it is **derived**
14from the microscopic entropy functional of quantum statistics.
15
16## What is proved
17
18For the dimensionless radiation integrals (x = E/T):
19
20* **Bose–Einstein** (f = 1/(eˣ−1), entropy integrand
21 σ_B(x) = x²[(1+f)ln(1+f) − f ln f]):
22 `∫₀^∞ σ_B = 4π⁴/45 = (4/3)·∫₀^∞ x³/(eˣ−1)` (`bose_entropy_eq_four_thirds_energy`)
23
24* **Fermi–Dirac** (f = 1/(eˣ+1), entropy integrand
25 σ_F(x) = x²[−f ln f − (1−f)ln(1−f)]):
26 `∫₀^∞ σ_F = 7π⁴/90 = (4/3)·∫₀^∞ x³/(eˣ+1)` (`fermi_entropy_eq_four_thirds_energy`)
27
28* **The 7/8 entropy weight**: `∫σ_F / ∫σ_B = 7/8`
29 (`fermi_div_bose_entropy`) — the fermionic statistics factor now holds at
30 the *entropy-functional* layer, not only at the energy layer.
31
32* **The entropy coefficient**: `∫σ_B / (2π²) = 2π²/45`
33 (`entropy_coeff_from_functional`) — the `2π²/45` prefactor of
34 `s_γ = (2π²/45)·g·T³` emerges from the functional, with the 4/3 never
35 assumed.
36
37## Method
38
39The pointwise identity (proved in `bose_entropy_pointwise` /
40`fermi_entropy_pointwise`) splits each entropy integrand into the energy
41kernel plus a logarithmic kernel:
42
43* Bose: σ_B(x) = x³/(eˣ−1) + x²·(−ln(1−e^{−x}))
44* Fermi: σ_F(x) = x³/(eˣ+1) + x²·ln(1+e^{−x})
45
46The logarithmic kernels expand by `Real.hasSum_pow_div_log_of_abs_lt_one`
47(the Mercator series in e^{−x}), and their Mellin transforms at s = 3
48evaluate via `hasSum_mellin` to Γ(3)·ζ(4) = π⁴/45 (Bose) and
49Γ(3)·η(4) = 7π⁴/360 (Fermi). Combined with the energy integrals π⁴/15 and
507π⁴/120 (`FermionWeightIntegral`), the totals are 4π⁴/45 and 7π⁴/90, which
51are exactly 4/3 of the energy integrals. Integrability of each piece is
52extracted by contraposition from the nonvanishing of its computed value.
53
54## What remains MODEL upstream
55
56The phase-space normalization g/(2π²) (degeneracy count and ℏ=c=k_B=1
57units) and the identification of the *physical* entropy density with the
58ideal-gas entropy functional are definitional bridges; all functional and
59numerical content of `s = (4/3)ρ/T` and of the 7/8 weight is THEOREM.
60-/
61
62namespace IndisputableMonolith
63namespace Cosmology
64namespace RadiationEntropyRelation
65
66open Real MeasureTheory Set
67
68/-! ## §1. The logarithmic kernels and their Mercator expansions -/
69
70/-- The Bose logarithmic kernel `−ln(1−e^{−t})`, complex-valued for the
71Mellin machinery. -/
72noncomputable def boseLogKernel (t : ℝ) : ℂ :=
73 ((-Real.log (1 - Real.exp (-t)) : ℝ) : ℂ)
74
75/-- The Fermi logarithmic kernel `ln(1+e^{−t})`, complex-valued for the
76Mellin machinery. -/
77noncomputable def fermiLogKernel (t : ℝ) : ℂ :=
78 ((Real.log (1 + Real.exp (-t)) : ℝ) : ℂ)
79
80/-- Mercator expansion `−ln(1−e^{−t}) = ∑_{n≥0} (e^{−t})^{n+1}/(n+1)` for `t > 0`. -/
81lemma boseLog_series {t : ℝ} (ht : 0 < t) :
82 HasSum (fun n : ℕ => Real.exp (-t) ^ (n + 1) / ((n : ℝ) + 1))
83 (-Real.log (1 - Real.exp (-t))) := by
84 have habs : |Real.exp (-t)| < 1 := by
85 rw [abs_of_pos (Real.exp_pos _)]
86 exact Real.exp_lt_one_iff.mpr (by linarith)
87 exact (Real.hasSum_pow_div_log_of_abs_lt_one habs).congr_fun
88 fun n => by ring
89
90/-- Mercator expansion `ln(1+e^{−t}) = ∑_{n≥0} (−1)ⁿ (e^{−t})^{n+1}/(n+1)`
91for `t > 0`. -/
92lemma fermiLog_series {t : ℝ} (ht : 0 < t) :
93 HasSum (fun n : ℕ => (-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1) / ((n : ℝ) + 1))
94 (Real.log (1 + Real.exp (-t))) := by
95 have habs : |(-Real.exp (-t))| < 1 := by
96 rw [abs_neg, abs_of_pos (Real.exp_pos _)]
97 exact Real.exp_lt_one_iff.mpr (by linarith)
98 have h := (Real.hasSum_pow_div_log_of_abs_lt_one habs).neg
99 have hval : -(-Real.log (1 - -Real.exp (-t))) = Real.log (1 + Real.exp (-t)) := by
100 rw [neg_neg, sub_neg_eq_add]
101 rw [hval] at h
102 refine h.congr_fun fun n => ?_
103 rw [neg_pow, pow_succ]
104 ring
105
106/-! ## §2. Summability of the weighted coefficient norms -/
107
108/-- Summability of `‖1/(n+1)‖ / (n+1)³`, as required by `hasSum_mellin`
109for the Bose logarithmic kernel. -/
110lemma summable_norm_boseLog :
111 Summable (fun n : ℕ =>
112 ‖((1 / ((n : ℝ) + 1) : ℝ) : ℂ)‖ / ((n : ℝ) + 1) ^ ((3 : ℂ)).re) := by
113 refine FermionWeightIntegral.summable_shift_rpow.congr fun n => ?_
114 have hpos : (0 : ℝ) < (n : ℝ) + 1 := by positivity
115 have h1 : ‖((1 / ((n : ℝ) + 1) : ℝ) : ℂ)‖ = 1 / ((n : ℝ) + 1) := by
116 rw [Complex.norm_real, Real.norm_eq_abs]
117 exact abs_of_pos (by positivity)
118 rw [h1, show ((3 : ℂ)).re = (3 : ℝ) by norm_num,
119 show (4 : ℝ) = (3 : ℝ) + 1 by norm_num, Real.rpow_add hpos, Real.rpow_one,
120 div_div, mul_comm (((n : ℝ) + 1) ^ (3 : ℝ)) ((n : ℝ) + 1)]
121
122/-- Summability of `‖(−1)ⁿ/(n+1)‖ / (n+1)³`, as required by `hasSum_mellin`
123for the Fermi logarithmic kernel. -/
124lemma summable_norm_fermiLog :
125 Summable (fun n : ℕ =>
126 ‖(((-1 : ℝ) ^ n / ((n : ℝ) + 1) : ℝ) : ℂ)‖ / ((n : ℝ) + 1) ^ ((3 : ℂ)).re) := by
127 refine FermionWeightIntegral.summable_shift_rpow.congr fun n => ?_
128 have hpos : (0 : ℝ) < (n : ℝ) + 1 := by positivity
129 have h1 : ‖(((-1 : ℝ) ^ n / ((n : ℝ) + 1) : ℝ) : ℂ)‖ = 1 / ((n : ℝ) + 1) := by
130 rw [Complex.norm_real, Real.norm_eq_abs, abs_div, abs_pow, abs_neg, abs_one,
131 one_pow, abs_of_pos hpos]
132 rw [h1, show ((3 : ℂ)).re = (3 : ℝ) by norm_num,
133 show (4 : ℝ) = (3 : ℝ) + 1 by norm_num, Real.rpow_add hpos, Real.rpow_one,
134 div_div, mul_comm (((n : ℝ) + 1) ^ (3 : ℝ)) ((n : ℝ) + 1)]
135
136/-! ## §3. Mellin transforms of the logarithmic kernels at s = 3 -/
137
138/-- Mellin/Dirichlet identity for the Bose logarithmic kernel at `s = 3`. -/
139lemma hasSum_mellin_boseLog :
140 HasSum (fun n : ℕ =>
141 Complex.Gamma 3 * ((1 / ((n : ℝ) + 1) : ℝ) : ℂ)
142 / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (3 : ℂ))
143 (mellin boseLogKernel 3) := by
144 refine hasSum_mellin (a := fun n : ℕ => ((1 / ((n : ℝ) + 1) : ℝ) : ℂ))
145 (p := fun n : ℕ => (n : ℝ) + 1) (F := boseLogKernel) (s := 3)
146 (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
147 · have ht' : (0 : ℝ) < t := ht
148 have hC : HasSum
149 (fun n : ℕ => ((Real.exp (-t) ^ (n + 1) / ((n : ℝ) + 1) : ℝ) : ℂ))
150 (boseLogKernel t) := Complex.hasSum_ofReal.mpr (boseLog_series ht')
151 refine hC.congr_fun fun n => ?_
152 have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
153 rw [← Real.exp_nat_mul]
154 congr 1
155 push_cast
156 ring
157 rw [hexp]
158 push_cast
159 ring
160 · exact summable_norm_boseLog
161
162/-- Mellin/Dirichlet identity for the Fermi logarithmic kernel at `s = 3`. -/
163lemma hasSum_mellin_fermiLog :
164 HasSum (fun n : ℕ =>
165 Complex.Gamma 3 * (((-1 : ℝ) ^ n / ((n : ℝ) + 1) : ℝ) : ℂ)
166 / (((n : ℝ) + 1 : ℝ) : ℂ) ^ (3 : ℂ))
167 (mellin fermiLogKernel 3) := by
168 refine hasSum_mellin (a := fun n : ℕ => (((-1 : ℝ) ^ n / ((n : ℝ) + 1) : ℝ) : ℂ))
169 (p := fun n : ℕ => (n : ℝ) + 1) (F := fermiLogKernel) (s := 3)
170 (fun i => Or.inr (by positivity)) (by norm_num) (fun t ht => ?_) ?_
171 · have ht' : (0 : ℝ) < t := ht
172 have hC : HasSum
173 (fun n : ℕ =>
174 (((-1 : ℝ) ^ n * Real.exp (-t) ^ (n + 1) / ((n : ℝ) + 1) : ℝ) : ℂ))
175 (fermiLogKernel t) := Complex.hasSum_ofReal.mpr (fermiLog_series ht')
176 refine hC.congr_fun fun n => ?_
177 have hexp : Real.exp (-((n : ℝ) + 1) * t) = Real.exp (-t) ^ (n + 1) := by
178 rw [← Real.exp_nat_mul]
179 congr 1
180 push_cast
181 ring
182 rw [hexp]
183 push_cast
184 ring
185 · exact summable_norm_fermiLog
186
187/-! ## §4. Closed-form values of the logarithmic Mellin transforms -/
188
189/-- `mellin (−ln(1−e^{−t})) 3 = Γ(3)·ζ(4) = π⁴/45`. -/
190lemma mellin_boseLog_value : mellin boseLogKernel 3 = ((π ^ 4 / 45 : ℝ) : ℂ) := by
191 refine hasSum_mellin_boseLog.unique ?_
192 have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((1 : ℝ) / ((n : ℝ) + 1) ^ 4))
193 (π ^ 4 / 45) := by
194 have h := FermionWeightIntegral.hasSum_zeta_shift.mul_left 2
195 convert h using 1
196 ring
197 have hC := Complex.hasSum_ofReal.mpr hre
198 refine hC.congr_fun fun n => ?_
199 rw [NumberDensityIntegral.gamma_three, NumberDensityIntegral.cpow_shift3 n]
200 have hne : ((n : ℂ) + 1) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero n
201 push_cast
202 field_simp
203
204/-- `mellin (ln(1+e^{−t})) 3 = Γ(3)·η(4) = 7π⁴/360`. -/
205lemma mellin_fermiLog_value :
206 mellin fermiLogKernel 3 = ((7 * π ^ 4 / 360 : ℝ) : ℂ) := by
207 refine hasSum_mellin_fermiLog.unique ?_
208 have hre : HasSum (fun n : ℕ => (2 : ℝ) * ((-1 : ℝ) ^ n / ((n : ℝ) + 1) ^ 4))
209 (7 * π ^ 4 / 360) := by
210 have h := FermionWeightIntegral.hasSum_eta_shift.mul_left 2
211 convert h using 1
212 ring
213 have hC := Complex.hasSum_ofReal.mpr hre
214 refine hC.congr_fun fun n => ?_
215 rw [NumberDensityIntegral.gamma_three, NumberDensityIntegral.cpow_shift3 n]
216 have hne : ((n : ℂ) + 1) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero n
217 push_cast
218 field_simp
219
220/-! ## §5. The Mellin transforms are the logarithmic integrals -/
221
222/-- `mellin boseLogKernel 3` is the (complexified) Bose logarithmic integral. -/
223lemma mellin_boseLog_eq_integral :
224 mellin boseLogKernel 3
225 = (((∫ t in Ioi (0 : ℝ), t ^ 2 * (-Real.log (1 - Real.exp (-t))) : ℝ)) : ℂ) := by
226 have h1 : mellin boseLogKernel 3
227 = ∫ t in Ioi (0 : ℝ), ((t ^ 2 * (-Real.log (1 - Real.exp (-t))) : ℝ) : ℂ) := by
228 unfold mellin
229 refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
230 rw [smul_eq_mul, show (3 : ℂ) - 1 = ((2 : ℕ) : ℂ) by norm_num,
231 Complex.cpow_natCast]
232 unfold boseLogKernel
233 push_cast
234 ring
235 rw [h1, integral_complex_ofReal]
236
237/-- `mellin fermiLogKernel 3` is the (complexified) Fermi logarithmic integral. -/
238lemma mellin_fermiLog_eq_integral :
239 mellin fermiLogKernel 3
240 = (((∫ t in Ioi (0 : ℝ), t ^ 2 * Real.log (1 + Real.exp (-t)) : ℝ)) : ℂ) := by
241 have h1 : mellin fermiLogKernel 3
242 = ∫ t in Ioi (0 : ℝ), ((t ^ 2 * Real.log (1 + Real.exp (-t)) : ℝ) : ℂ) := by
243 unfold mellin
244 refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
245 rw [smul_eq_mul, show (3 : ℂ) - 1 = ((2 : ℕ) : ℂ) by norm_num,
246 Complex.cpow_natCast]
247 unfold fermiLogKernel
248 push_cast
249 ring
250 rw [h1, integral_complex_ofReal]
251
252/-! ## §6. The logarithmic integrals in closed form -/
253
254/-- **THEOREM.** `∫₀^∞ t²·(−ln(1−e^{−t})) dt = π⁴/45`. -/
255theorem boseLog_integral_value :
256 (∫ t in Ioi (0 : ℝ), t ^ 2 * (-Real.log (1 - Real.exp (-t)))) = π ^ 4 / 45 := by
257 have h := mellin_boseLog_value
258 rw [mellin_boseLog_eq_integral] at h
259 exact Complex.ofReal_inj.mp h
260
261/-- **THEOREM.** `∫₀^∞ t²·ln(1+e^{−t}) dt = 7π⁴/360`. -/
262theorem fermiLog_integral_value :
263 (∫ t in Ioi (0 : ℝ), t ^ 2 * Real.log (1 + Real.exp (-t))) = 7 * π ^ 4 / 360 := by
264 have h := mellin_fermiLog_value
265 rw [mellin_fermiLog_eq_integral] at h
266 exact Complex.ofReal_inj.mp h
267
268/-! ## §7. The entropy integrands and their pointwise decomposition -/
269
270/-- The Bose–Einstein entropy integrand
271`σ_B(t) = t²[(1+f)ln(1+f) − f ln f]` with `f = 1/(eᵗ−1)`. -/
272noncomputable def boseEntropyIntegrand (t : ℝ) : ℝ :=
273 t ^ 2 * ((1 + 1 / (Real.exp t - 1)) * Real.log (1 + 1 / (Real.exp t - 1))
274 - (1 / (Real.exp t - 1)) * Real.log (1 / (Real.exp t - 1)))
275
276/-- The Fermi–Dirac entropy integrand
277`σ_F(t) = t²[−f ln f − (1−f)ln(1−f)]` with `f = 1/(eᵗ+1)`. -/
278noncomputable def fermiEntropyIntegrand (t : ℝ) : ℝ :=
279 t ^ 2 * (-(1 / (Real.exp t + 1)) * Real.log (1 / (Real.exp t + 1))
280 - (1 - 1 / (Real.exp t + 1)) * Real.log (1 - 1 / (Real.exp t + 1)))
281
282/-- **Pointwise decomposition (Bose).** For `t > 0`,
283`σ_B(t) = t³/(eᵗ−1) + t²·(−ln(1−e^{−t}))`: the entropy integrand is the
284energy kernel plus the logarithmic kernel. -/
285lemma bose_entropy_pointwise {t : ℝ} (ht : 0 < t) :
286 boseEntropyIntegrand t
287 = t ^ 3 / (Real.exp t - 1) + t ^ 2 * (-Real.log (1 - Real.exp (-t))) := by
288 have hE1 : (1 : ℝ) < Real.exp t := by
289 rw [← Real.exp_zero]
290 exact Real.exp_lt_exp.mpr ht
291 have hEpos : (0 : ℝ) < Real.exp t := Real.exp_pos t
292 have hne : Real.exp t - 1 ≠ 0 := by linarith
293 have hlog1f : Real.log (1 + 1 / (Real.exp t - 1))
294 = t - Real.log (Real.exp t - 1) := by
295 have hval : (1 : ℝ) + 1 / (Real.exp t - 1) = Real.exp t / (Real.exp t - 1) := by
296 field_simp
297 ring
298 rw [hval, Real.log_div hEpos.ne' hne, Real.log_exp]
299 have hlogf : Real.log (1 / (Real.exp t - 1)) = -Real.log (Real.exp t - 1) := by
300 rw [one_div, Real.log_inv]
301 have hlogm : Real.log (1 - Real.exp (-t)) = Real.log (Real.exp t - 1) - t := by
302 have hval : (1 : ℝ) - Real.exp (-t) = (Real.exp t - 1) / Real.exp t := by
303 rw [Real.exp_neg]
304 field_simp
305 rw [hval, Real.log_div hne hEpos.ne', Real.log_exp]
306 unfold boseEntropyIntegrand
307 rw [hlog1f, hlogf, hlogm]
308 ring
309
310/-- **Pointwise decomposition (Fermi).** For `t > 0`,
311`σ_F(t) = t³/(eᵗ+1) + t²·ln(1+e^{−t})`: the entropy integrand is the
312energy kernel plus the logarithmic kernel. -/
313lemma fermi_entropy_pointwise {t : ℝ} (_ht : 0 < t) :
314 fermiEntropyIntegrand t
315 = t ^ 3 / (Real.exp t + 1) + t ^ 2 * Real.log (1 + Real.exp (-t)) := by
316 have hEpos : (0 : ℝ) < Real.exp t := Real.exp_pos t
317 have hne : Real.exp t + 1 ≠ 0 := by positivity
318 have hlogf : Real.log (1 / (Real.exp t + 1)) = -Real.log (Real.exp t + 1) := by
319 rw [one_div, Real.log_inv]
320 have hlog1f : Real.log (1 - 1 / (Real.exp t + 1))
321 = t - Real.log (Real.exp t + 1) := by
322 have hval : (1 : ℝ) - 1 / (Real.exp t + 1) = Real.exp t / (Real.exp t + 1) := by
323 field_simp
324 ring
325 rw [hval, Real.log_div hEpos.ne' hne, Real.log_exp]
326 have hlogp : Real.log (1 + Real.exp (-t)) = Real.log (Real.exp t + 1) - t := by
327 have hval : (1 : ℝ) + Real.exp (-t) = (Real.exp t + 1) / Real.exp t := by
328 rw [Real.exp_neg]
329 field_simp
330 rw [hval, Real.log_div hne hEpos.ne', Real.log_exp]
331 unfold fermiEntropyIntegrand
332 rw [hlogf, hlog1f, hlogp]
333 ring
334
335/-! ## §8. Integrability of the pieces (by contraposition from the values) -/
336
337/-- The Bose energy kernel is integrable on `(0,∞)` (its integral is `π⁴/15 ≠ 0`). -/
338lemma integrableOn_bose_energy :
339 IntegrableOn (fun t : ℝ => t ^ 3 / (Real.exp t - 1)) (Ioi (0 : ℝ)) := by
340 by_contra hcon
341 have h0 : (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1)) = 0 :=
342 integral_undef hcon
343 rw [FermionWeightIntegral.bose_integral_value] at h0
344 have hpos : (0 : ℝ) < π ^ 4 / 15 := by positivity
345 linarith
346
347/-- The Bose logarithmic kernel is integrable on `(0,∞)`
348(its integral is `π⁴/45 ≠ 0`). -/
349lemma integrableOn_boseLog :
350 IntegrableOn (fun t : ℝ => t ^ 2 * (-Real.log (1 - Real.exp (-t))))
351 (Ioi (0 : ℝ)) := by
352 by_contra hcon
353 have h0 : (∫ t in Ioi (0 : ℝ), t ^ 2 * (-Real.log (1 - Real.exp (-t)))) = 0 :=
354 integral_undef hcon
355 rw [boseLog_integral_value] at h0
356 have hpos : (0 : ℝ) < π ^ 4 / 45 := by positivity
357 linarith
358
359/-- The Fermi energy kernel is integrable on `(0,∞)`
360(its integral is `7π⁴/120 ≠ 0`). -/
361lemma integrableOn_fermi_energy :
362 IntegrableOn (fun t : ℝ => t ^ 3 / (Real.exp t + 1)) (Ioi (0 : ℝ)) := by
363 by_contra hcon
364 have h0 : (∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1)) = 0 :=
365 integral_undef hcon
366 rw [FermionWeightIntegral.fermi_integral_value] at h0
367 have hpos : (0 : ℝ) < 7 * π ^ 4 / 120 := by positivity
368 linarith
369
370/-- The Fermi logarithmic kernel is integrable on `(0,∞)`
371(its integral is `7π⁴/360 ≠ 0`). -/
372lemma integrableOn_fermiLog :
373 IntegrableOn (fun t : ℝ => t ^ 2 * Real.log (1 + Real.exp (-t)))
374 (Ioi (0 : ℝ)) := by
375 by_contra hcon
376 have h0 : (∫ t in Ioi (0 : ℝ), t ^ 2 * Real.log (1 + Real.exp (-t))) = 0 :=
377 integral_undef hcon
378 rw [fermiLog_integral_value] at h0
379 have hpos : (0 : ℝ) < 7 * π ^ 4 / 360 := by positivity
380 linarith
381
382/-! ## §9. The entropy integrals in closed form -/
383
384/-- **THEOREM (Bose entropy integral).**
385`∫₀^∞ t²[(1+f)ln(1+f) − f ln f] dt = 4π⁴/45` with `f = 1/(eᵗ−1)`. -/
386theorem bose_entropy_integral_value :
387 (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) = 4 * π ^ 4 / 45 := by
388 have hsplit : (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t)
389 = ∫ t in Ioi (0 : ℝ),
390 (t ^ 3 / (Real.exp t - 1) + t ^ 2 * (-Real.log (1 - Real.exp (-t)))) := by
391 refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
392 exact bose_entropy_pointwise ht
393 rw [hsplit, integral_add integrableOn_bose_energy integrableOn_boseLog,
394 FermionWeightIntegral.bose_integral_value, boseLog_integral_value]
395 ring
396
397/-- **THEOREM (Fermi entropy integral).**
398`∫₀^∞ t²[−f ln f − (1−f)ln(1−f)] dt = 7π⁴/90` with `f = 1/(eᵗ+1)`. -/
399theorem fermi_entropy_integral_value :
400 (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t) = 7 * π ^ 4 / 90 := by
401 have hsplit : (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
402 = ∫ t in Ioi (0 : ℝ),
403 (t ^ 3 / (Real.exp t + 1) + t ^ 2 * Real.log (1 + Real.exp (-t))) := by
404 refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
405 exact fermi_entropy_pointwise ht
406 rw [hsplit, integral_add integrableOn_fermi_energy integrableOn_fermiLog,
407 FermionWeightIntegral.fermi_integral_value, fermiLog_integral_value]
408 ring
409
410/-! ## §10. Capstones: s = (4/3)ρ/T, the 7/8 entropy weight, and 2π²/45 -/
411
412/-- **THEOREM (s = (4/3)ρ/T, Bose).** The Bose entropy integral is exactly
413`4/3` of the Bose energy integral. This is the dimensionless content of the
414thermodynamic relation `s = (4/3)·ρ/T` for a massless boson gas, derived from
415the microscopic entropy functional (never assumed). -/
416theorem bose_entropy_eq_four_thirds_energy :
417 (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t)
418 = 4 / 3 * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
419 rw [bose_entropy_integral_value, FermionWeightIntegral.bose_integral_value]
420 ring
421
422/-- **THEOREM (s = (4/3)ρ/T, Fermi).** The Fermi entropy integral is exactly
423`4/3` of the Fermi energy integral: the same 4/3 law holds for a massless
424fermion gas. -/
425theorem fermi_entropy_eq_four_thirds_energy :
426 (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
427 = 4 / 3 * ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1) := by
428 rw [fermi_entropy_integral_value, FermionWeightIntegral.fermi_integral_value]
429 ring
430
431/-- **THEOREM (7/8 at the entropy layer).** The Fermi entropy integral is
432exactly `7/8` of the Bose one: the fermionic statistics weight of
433`EntropyPerPhoton.fermionWeight` holds directly for entropy, not only for
434energy. -/
435theorem fermi_div_bose_entropy :
436 (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
437 / (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) = 7 / 8 := by
438 rw [bose_entropy_integral_value, fermi_entropy_integral_value]
439 rw [div_eq_iff (by positivity)]
440 ring
441
442/-- **THEOREM (entropy weight provenance, entropy layer).**
443`∫σ_F = fermionWeight · ∫σ_B` with the `7/8` MODEL constant of
444`EntropyPerPhoton.fermionWeight`. -/
445theorem fermi_entropy_eq_weight_mul_bose :
446 (∫ t in Ioi (0 : ℝ), fermiEntropyIntegrand t)
447 = ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
448 * ∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t := by
449 rw [bose_entropy_integral_value, fermi_entropy_integral_value]
450 unfold EntropyPerPhoton.fermionWeight
451 push_cast
452 ring
453
454/-- **THEOREM (the 2π²/45 entropy coefficient from the functional).**
455`s_γ = (g/2π²)·T³·∫σ_B = (2π²/45)·g·T³`: dividing the derived entropy
456integral by the phase-space normalization `2π²` yields exactly the `2π²/45`
457prefactor of the photon entropy density, with the `4/3` factor never
458assumed. -/
459theorem entropy_coeff_from_functional :
460 (∫ t in Ioi (0 : ℝ), boseEntropyIntegrand t) / (2 * π ^ 2) = 2 * π ^ 2 / 45 := by
461 rw [bose_entropy_integral_value]
462 rw [div_eq_iff (by positivity)]
463 ring
464
465end RadiationEntropyRelation
466end Cosmology
467end IndisputableMonolith
468