integrableOn_Ioi_of_rpow_decay
plain-language theorem explainer
Generic domination lemma establishing L1 integrability on (1,∞) for any continuous f dominated pointwise by C r^α whenever α < -1. Analysts closing decay estimates for ancient Navier-Stokes solutions cite it to convert radial power-law bounds into the L1 membership required by CoerciveL2Bound. The argument compares the target integrand to the known integrable majorant C r^α and applies a monotonicity property for the integral.
Claim. Let $f:ℝ→ℝ$ be continuous on $(1,∞)$. If $C>0$ and $α<-1$ satisfy $|f(r)|≤C r^α$ for all $r>1$, then $f$ is integrable over $(1,∞)$ with respect to Lebesgue measure.
background
In the RM2U Tail Flux Instantiation module, ancient Navier-Stokes elements extracted via Galerkin diagonal convergence obey energy decay A(r)=O(r^{-3/2}) at spatial infinity. CoerciveL2Bound is the concrete analytic target requiring both A² and (A')² r² to lie in L¹(1,∞); this supplies the domination tool that turns the power-law decay into those integrability statements. Upstream, CoerciveL2Bound is defined as the conjunction of those two integrability conditions and serves as the hypothesis structure that closes the RM2U argument once the decay is established.
proof idea
The term proof first applies integrableOn_Ioi_rpow_of_lt to obtain integrability of the majorant C r^α on (1,∞), scales by the constant C, and then invokes integrable.mono' using a.e. strong measurability from continuity together with the pointwise bound to dominate the absolute value.
why it matters
This lemma discharges the integrability halves of CoerciveL2Bound once AncientEnergyDecay supplies the decay exponents -3/2 and -5/2. It is invoked directly in ancientDecay_implies_A2_integrable and ancientDecay_implies_Aprime2r2_integrable, which feed operatorPairing_of_decayFull and the tail-flux vanishing conditions. In the Recognition framework it closes the analytic step that instantiates the RM2U hypothesis structure for concrete ancient solutions, advancing the chain from the energy inequality to Bet1 boundary-term integrability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.