mellin_bose3_eq_integral
plain-language theorem explainer
The Mellin transform of the Bose–Einstein kernel at order 3 equals the complexification of the real integral ∫_{0}^{∞} t²/(eᵗ−1) dt. Cosmologists cite it to pass between the Mellin/series layer and the classical number-density integral for photons. The proof unfolds the Mellin definition, matches integrands pointwise on (0,∞), then applies complex-of-real integral transport.
Claim. The Mellin transform of the Bose–Einstein kernel $1/(e^t-1)$ at $s=3$ equals the complexification of the real improper integral $\int_{(0,\infty)} t^2/(e^t-1)\,dt$.
background
This module closes the number-density layer of thermal integrals at Mellin order $s=3$, the companion of the energy-density work at $s=4$ in FermionWeightIntegral. Photon number density is $n_\gamma=(g_\gamma/(2\pi^2))T^3\int_0^\infty t^2/(e^t-1),dt$, so the real integral must be identified with a Mellin transform that the series layer can evaluate.
The Bose–Einstein kernel is the complex-valued map $t\mapsto 1/(e^t-1)$ used by the Mellin machinery. The Mellin transform at complex order $s$ multiplies the kernel by $t^{s-1}$ and integrates over $(0,\infty)$. At $s=3$ one has $t^{s-1}=t^2$, so the Mellin integrand is exactly the classical Bose number-density integrand, complexified.
The Fermi kernel $1/(e^t+1)$ is the parallel object for fermionic number densities; the same identification at $s=3$ yields the $3/4$ fermion number weight $\eta(3)/\zeta(3)$.
proof idea
Two steps. First, unfold the Mellin definition and use set-integral congruence on $(0,\infty)$: for $t>0$, the scalar factor $t^{3-1}$ is $t^2$ (via $3-1=2$ and natural-power complex exponentiation), and unfolding the Bose kernel plus push_cast/ring shows the complex integrand equals the complexification of $t^2/(e^t-1)$. Second, rewrite the resulting complex integral of a real-valued function as the complexification of the real integral via integral_complex_ofReal.
why it matters
This is the bridge lemma from the Mellin/series side to the classical real Bose number integral. Downstream, bose_number_integral_value rewrites the Mellin evaluation through this equality and obtains $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$, the analytic content of $n_\gamma=(2\zeta(3)/\pi^2)T^3$.
Together with the Fermi twin and the $s=4$ energy integrals, it supplies the last analytic ingredient of entropyPerPhoton_eq_ratio: the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$, the companion of the $7/8$ entropy weight that dilutes $n_\nu/n_\gamma$ before entropy dilution. In the Recognition cosmology stack this is pure thermodynamic bookkeeping, not a new forcing step, but it hardens the photon/neutrino number-density coefficients used by the entropy-per-photon capstone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.