bose_integral_value
plain-language theorem explainer
The Bose–Einstein energy integral equals π⁴/15 exactly: ∫₀^∞ t³/(eᵗ−1) dt = π⁴/15. Cosmology and statistical-mechanics arguments cite this as the closed form of the massless boson energy density. The proof transports the Mellin-transform evaluation at s=4 down to the real line integral by uniqueness of the complex embedding.
Claim. The improper integral $\int_{0}^{\infty} t^{3}/(e^{t}-1)\,dt$ equals $\pi^{4}/15$.
background
This module sits at the thermodynamic (integral) layer of the fermion-weight story. The sibling module FermionWeight already proved the series identity η(4)=(7/8)ζ(4). Here both Bose and Fermi energy integrals are realized as Mellin transforms at s=4 of geometric series in e^{−t}, so that Mathlib's Mellin–Dirichlet correspondence yields Γ(4)·ζ(4) and Γ(4)·η(4).
The Bose kernel is F(t)=1/(eᵗ−1)=∑{n≥0} e^{−(n+1)t} for t>0. Its Mellin transform at s=4 is ∑ Γ(4)·(n+1)^{−4}. With Γ(4)=6 and the shifted zeta sum equal to ζ(4)=π⁴/90, one obtains π⁴/15. The lemma mellin_bose_value records exactly that complex equality; mellin_bose_eq_integral identifies the Mellin transform with the complexification of the real energy integral ∫{t>0} t³/(eᵗ−1) dt.
proof idea
Three-line term proof. Start from mellin_bose_value, which asserts mellin(boseKernel,4)=π⁴/15 in ℂ. Rewrite the left-hand side via mellin_bose_eq_integral, which equates that Mellin value to the complexification of the real integral. Discharge the resulting equality of complex numbers by injectivity of the real-to-complex embedding (Complex.ofReal_inj).
why it matters
This is the Bose closed form that makes the entire 7/8 fermion-weight factor a theorem at the thermodynamic layer, not merely a series identity. Downstream, fermi_div_bose_integral divides the Fermi integral by this value to obtain 7/8; fermi_integral_eq_weight_mul_bose identifies that ratio with the MODEL constant EntropyPerPhoton.fermionWeight.
It also feeds the radiation bookkeeping: plasmaEnergy_eq inserts π⁴/15 (and 7π⁴/120) to recover ρ=(π²/30)(g_B+(7/8)g_F)T⁴; entropy_density_coeff_provenance and entropyPerPhoton_from_integrals derive the 2π²/45 coefficient and the entropy-per-photon formula from this integral; bose_entropy_eq_four_thirds_energy uses it to prove s=(4/3)ρ/T for a massless boson gas from the microscopic entropy functional. With these results, the only remaining MODEL content in the entropy-per-photon chain is the relativistic species census g*, not the statistics factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.