radial_scale_pow
plain-language theorem explainer
For any natural power n and positive temperature T, the radial integral ∫_{y>0} y^n K(y/T) dy equals T^{n+1} times the same integral at unit temperature. Cosmology proofs cite it to extract the Stefan–Boltzmann T^{D+1} factor from momentum-space kernels. The argument is a change of variables y = T t via Mathlib's left-multiplication substitution on (0,∞), followed by algebraic rearrangement of the power weight.
Claim. For every $n \in \mathbb{N}$, every measurable $K : \mathbb{R} \to \mathbb{R}$, and every $T > 0$, $$\int_{(0,\infty)} y^n\, K(y/T)\, dy = T^{n+1} \int_{(0,\infty)} t^n\, K(t)\, dt.$$
background
The module PhaseSpaceReduction derives the standard 1D plasma integrals $P = (g/2\pi^2), T^4 \int t^2 K(t), dt$ from the underlying 3D momentum integral $(g/(2\pi)^3)\int d^3k, T, K(|k|/T)$. The angular factor $4\pi/(2\pi)^3 = 1/(2\pi^2)$ and the $T^4$ scaling were previously baked into the definitions; here both are proved from co-area reduction and the substitution $k = T\cdot t$.
This lemma isolates the pure radial scaling step. After the Haar integral of a norm-dependent integrand collapses to a 1D integral against the surface measure (weight $y^{d-1}$ in dimension $d$), one still needs to pull temperature out of $\int y^n K(y/T), dy$. The result is unconditional: Mathlib change-of-variables lemmas hold in junk-value semantics on both sides, so no integrability hypothesis appears.
Upstream, $D = 3$ is forced by the Recognition chain (T8). The Stefan–Boltzmann exponent 4 is then structural: it is $D+1$, not an independent input.
proof idea
Fix $T > 0$, so $T^{-1} > 0$. Apply Mathlib's integral_comp_mul_left_Ioi to
the map $x \mapsto x^n K(x)$ with left-multiplication by $T^{-1}$ on $(0,\infty)$.
That yields
$$\int_{(0,\infty)} (T^{-1}x)^n K(T^{-1}x), dx = T \int_{(0,\infty)} x^n K(x), dx.$$
Separately, pointwise identity shows
$y^n K(y/T) = T^n \bigl((T^{-1} y)^n K(T^{-1} y)\bigr)$, using $T^n (y/T)^n = y^n$
(via div_pow and field simplification) and inv_mul_eq_div. Substitute the
identity under the integral, factor the constant $T^n$ with integral_const_mul,
combine with the change-of-variables identity, and finish by ring to obtain
the factor $T^{n+1}$.
why it matters
This is the temperature-extraction engine for the whole phase-space reduction.
phaseSpaceDensity_reduction invokes it (after the $D=3$ radial collapse) to
produce the closed form $(g/2\pi^2), T^4 \int t^2 K(t), dt$; the $T^4$ is exactly
$T\cdot T^3 = T^{D+1}$ from kernel rescaling plus this substitution. The same
lemma feeds phaseSpaceDensity_T_scaling, which proves $P_d(T) = T^{d+1} P_d(1)$
in any nonzero dimension without evaluating the unit-ball volume.
In the Recognition framework the exponent is not free: T8 forces $D=3$, so the classical Stefan–Boltzmann $T^4$ law is a corollary of dimension forcing rather than an empirical fit. The lemma is kernel-agnostic (pressure, energy, entropy, number density), matching the module claim that nothing about $K$ is used beyond the radial weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.