boseLog_integral_value
plain-language theorem explainer
The improper integral ∫₀^∞ t²(−ln(1−e^{−t})) dt equals π⁴/45. Cosmologists and statistical-mechanics workers cite this closed form when collapsing Bose radiation pressure and entropy functionals to elementary constants. The proof identifies the real integral with the Mellin transform of the Bose log kernel at order 3, then reads off the known value Γ(3)ζ(4)=π⁴/45 via complex-to-real injectivity.
Claim. The improper integral $\int_0^\infty t^2(-\ln(1-e^{-t}))\,dt$ equals $\pi^4/45$.
background
In the radiation-entropy module the microscopic Bose entropy integrand splits pointwise into an energy kernel plus a logarithmic kernel: σ_B(x)=x³/(e^x−1)+x²(−ln(1−e^{−x})). The log piece must be evaluated before the thermodynamic identity s=(4/3)·ρ/T can be derived from the entropy functional rather than assumed.
The Bose log kernel is t ↦ −ln(1−e^{−t}). Its Mellin transform at s=3 is the complexified integral of t² times that kernel. Upstream, mellin_boseLog_value evaluates that Mellin transform as Γ(3)ζ(4)=π⁴/45 in ℂ, via the series expansion of the kernel and the shifted zeta sum. The companion lemma mellin_boseLog_eq_integral unwraps the Mellin definition back into the complexification of the real improper integral on (0,∞).
proof idea
One-line bridge between two upstream lemmas. Start from mellin_boseLog_value (Mellin of the Bose log kernel at 3 equals π⁴/45 in ℂ). Rewrite the left-hand side by mellin_boseLog_eq_integral, which replaces the Mellin symbol by the complexification of ∫_{t>0} t²(−ln(1−e^{−t})) dt. Apply injectivity of the real embedding ℝ→ℂ to recover the real equality.
why it matters
This is the Bose half of the log-kernel evaluations that close plasma pressure in GrandPotential: plasmaPressure_eq rewrites the pressure integrals and obtains P=(π²/90)·(g_B+(7/8)g_F)·T⁴, with the 7/8 emerging independently in the pressure channel. Downstream, bose_entropy_integral_value adds this π⁴/45 to the Bose energy integral π⁴/15 (after the pointwise split) to get the full entropy integral 4π⁴/45, which is exactly (4/3) times the energy density integral. Integrability of the kernel on (0,∞) is recovered by contradiction from the nonzero value. In the η_B chain the result discharges the statistical-mechanics identification of the radiation entropy relation without thermodynamic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.