integrableOn_bose_energy
plain-language theorem explainer
The Bose–Einstein energy density kernel t³/(eᵗ−1) is Lebesgue-integrable on (0,∞). Cosmology and statistical-mechanics arguments that split the entropy functional into energy plus log pieces cite this to justify the energy integral. The proof is a short contradiction: non-integrability would force the integral to 0, but the known value π⁴/15 is strictly positive.
Claim. The map $t \mapsto t^3/(e^t-1)$ is integrable on $(0,\infty)$. In particular its improper integral exists as a real number (and equals $\pi^4/15$).
background
This module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than inserting the thermodynamic factor by hand. For Bose statistics the entropy integrand splits pointwise as
$$\sigma_B(t)=\frac{t^3}{e^t-1}+t^2\bigl(-\ln(1-e^{-t})\bigr).$$
The first summand is the classical Bose energy kernel. Upstream, bose_integral_value already evaluates its integral:
$$\int_0^\infty t^3/(e^t-1),dt=\pi^4/15.$$
Mathlib treats the integral of a non-integrable function as zero, so existence of a nonzero value is equivalent to integrability on $(0,\infty)$. That existence lemma is what this declaration records.
proof idea
Proof by contradiction. Assume the energy kernel is not integrable on $(0,\infty)$. Then Mathlib’s integral_undef forces
$$\int_{(0,\infty)} t^3/(e^t-1),dt=0.$$
Rewrite the left-hand side with the upstream theorem bose_integral_value, obtaining $\pi^4/15=0$. Positivity gives $0<\pi^4/15$, and linarith closes the contradiction. No series expansion or Mellin analysis is repeated here; the lemma only packages the nonzero evaluation into an IntegrableOn fact.
why it matters
Downstream, bose_entropy_integral_value splits the Bose entropy integrand into energy kernel plus logarithmic kernel and integrates termwise. Integrability of the energy piece is required before that split can be justified under the integral sign and before the identity
$$\int\sigma_B=4\pi^4/45=(4/3)\int t^3/(e^t-1)$$
can be stated. That identity is the Bose half of the module’s main claim: the factor $4/3$ in $s=(4/3)\rho/T$ emerges from the entropy functional, closing a MODEL step in the $\eta_B$ chain without thermodynamic input. The companion Fermi statements and the $7/8$ entropy weight rest on the same pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.