mellin_fermi_eq_integral
plain-language theorem explainer
The Mellin transform of the Fermi–Dirac kernel at s=4 equals the complexification of the real integral ∫₀^∞ t³/(eᵗ+1) dt. Cosmology and statistical-mechanics arguments that move between the Mellin/Dirichlet side and the thermodynamic energy integral cite this identification. The proof unfolds the Mellin definition, matches the integrand by elementary complex arithmetic, and applies the ofReal integral lemma.
Claim. The Mellin transform of the Fermi–Dirac kernel $F(t)=1/(e^{t}+1)$ at $s=4$ equals the complexification of the real improper integral: $\mathrm{Mellin}(F)(4)=\Bigl(\int_{0}^{\infty}\frac{t^{3}}{e^{t}+1}\,dt\Bigr)_{\mathbb{C}}$.
background
This module sits at the thermodynamic (integral) layer of the fermion-weight story. The companion module FermionWeight already gives the series identity η(4)=(7/8)·ζ(4). Here one must connect that Dirichlet side to the energy integrals that appear in entropy-per-photon bookkeeping:
$$\int_{0}^{\infty}\frac{t^{3}}{e^{t}+1},dt=\frac78\int_{0}^{\infty}\frac{t^{3}}{e^{t}-1},dt.$$
The Fermi–Dirac kernel is the complex-valued function $F(t)=(1/(e^{t}+1):\mathbb{R}):\mathbb{C}$, introduced so that Mathlib's Mellin transform applies. By definition the Mellin transform at $s=4$ multiplies the kernel by $t^{s-1}=t^{3}$ and integrates over $(0,\infty)$. The present lemma simply records that this abstract Mellin object is exactly the complexification of the classical real Fermi–Dirac integral.
proof idea
Two short steps. First, unfold the Mellin definition and apply set-integral congruence on Ioi 0. On each $t>0$ the integrand identity is pure arithmetic: $s-1=3$ at $s=4$, Complex.cpow_natCast turns the complex power into $t^{3}$, unfolding the Fermi kernel and push_cast/ring finish the pointwise match. Second, rewrite the resulting complex integral of a real-valued function via integral_complex_ofReal, which yields the claimed equality with the complexification of the real integral.
why it matters
Parent theorem fermi_integral_value rewrites through this lemma: once the Mellin side is known to equal Γ(4)·η(4)=6·(7/8)·π⁴/90=7π⁴/120, the real Fermi–Dirac integral inherits the same closed form. Together with the Bose twin, this closes the entire mathematical content of EntropyPerPhoton.fermionWeight=7/8. Only the physics census of relativistic species (the $g_{*}$ bookkeeping) remains model-level; the 7/8 statistics factor itself is theorem. The module status line is explicit: axiom-clean, Lean's base three only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.