integral_norm_fin_three
plain-language theorem explainer
A radial Haar integral of a norm-dependent function over Euclidean 3-space equals 4π times the weighted half-line integral ∫ y² f(y) dy. Cosmology and statistical-mechanics arguments that start from ∫ d³k g(‖k‖) cite this to collapse momentum space to a single radial coordinate. The proof applies Mathlib's co-area formula for additive Haar measure, inserts vol(B³)=4π/3, and simplifies the resulting angular prefactor 3·(4π/3)=4π.
Claim. For any $f:\mathbb{R}\to\mathbb{R}$, $$\int_{k\in\mathbb{R}^3} f(\|k\|)\,d^3k \;=\; 4\pi \int_0^\infty y^2 f(y)\,dy,$$ where the left-hand side is the Lebesgue (Haar) integral on Euclidean 3-space and the right-hand side is the ordinary improper integral on $(0,\infty)$.
background
The module PhaseSpaceReduction derives the textbook plasma prefactor $g/(2\pi^2)\cdot T^4$ from the underlying three-dimensional momentum integral, rather than baking it into the definition of grand potential. The starting object is $$P = \frac{g}{(2\pi)^3}\int d^3k; T,K(|k|/T),$$ and the first step is to replace the $\mathbb{R}^3$ integral by a radial line integral.
Mathlib supplies the general co-area identity integral_fun_norm_addHaar: for any finite-dimensional real inner-product space the integral of a radial function factors as (surface measure of the unit sphere) times $\int_0^\infty r^{d-1} f(r),dr$. In dimension three the surface factor is recovered from the unit-ball volume via $d\cdot\mathrm{vol}(B^d)$: here $\mathrm{vol}(B^3)=4\pi/3$, so the angular weight is $3\cdot(4\pi/3)=4\pi$.
Both sides are interpreted in Mathlib's junk-value semantics, so the identity is unconditional (no integrability hypothesis). The spatial dimension $D=3$ itself is not an input: it is forced upstream by T8 of the Unified Forcing Chain.
proof idea
Invoke MeasureTheory.integral_fun_norm_addHaar on Euclidean space of type Fin 3. Simplify the ambient dimension with finrank_euclideanSpace and Fintype.card_fin, obtaining a formula whose angular coefficient is $3$ times the real volume of the unit ball.
Compute that volume separately: EuclideanSpace.volume_ball_fin_three gives $\pi\cdot 4/3$ after converting the ENNReal measure to a real via measureReal_def and ENNReal.toReal_ofReal (positivity discharges the side condition). Substitute the ball volume, clear scalar multiplications with nsmul_eq_mul / smul_eq_mul, push casts, and finish by ring, which rearranges $3\cdot(4\pi/3)$ into $4\pi$.
why it matters
This is the angular half of the phase-space reduction that turns the 3D grand-canonical integral into the 1D form used throughout RS cosmology. The sole downstream consumer is phaseSpaceDensity_reduction, which quotes the identity on $f(y)=T,K(y/T)$ and then performs the temperature substitution $y=T t$ to extract $T^4$ and the mode-density factor $4\pi/(2\pi)^3=1/(2\pi^2)$.
In the Recognition framework the Stefan–Boltzmann exponent 4 is not an independent constant: it is $D+1$ with $D=3$, and $D=3$ is the T8 forcing theorem. By making the $4\pi$ factor a proved consequence of Haar measure on $\mathbb{R}^3$ rather than a modelling assumption, the module closes the provenance gap between the abstract forcing chain and the concrete plasma pressure/energy closed forms (phaseSpacePressure_closed_form, phaseSpaceEnergy_closed_form).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.