tail_integral_tendsto_zero
plain-language theorem explainer
If a real-valued function g is Lebesgue integrable over (1, ∞), its tail integrals from R onward vanish as R tends to infinity. Analysts working on decay estimates for PDEs on half-lines cite this for controlling remainders in Sobolev embeddings. The argument splits the tail as the full integral minus the integral up to R, invokes continuity of the indefinite integral at infinity, and transfers the limit via eventual equality of the expressions.
Claim. Let $g : (1,∞) → ℝ$ be Lebesgue integrable. Then $∫_R^∞ g(x) dx → 0$ as $R → ∞$.
background
This lemma sits inside the RM2U Tail Flux Instantiation module, which connects Galerkin-extracted ancient Navier-Stokes elements to the Bet1 integrability conditions required for coercivity. The module assumes an energy-bounded velocity field whose ℓ=2 spherical-harmonic projection yields a radial profile A(r) satisfying ∫ A(r)² r² dr < ∞ on (1,∞), which in turn implies the L¹ tail hypothesis used here. IntegrableOn g (Ioi 1) volume means the Lebesgue integral of |g| over (1,∞) is finite; the local setting therefore treats the half-line as the radial coordinate after Parseval reduction on the sphere.
proof idea
The tactic proof first applies intervalIntegral_tendsto_integral_Ioi to obtain convergence of the integral from 1 to R to the full integral over (1,∞). It then decomposes the tail integral as the difference of the full integral minus the integral up to R for R ≥ 1, using disjointness of Ioc(1,R) and Ioi R together with the union identity Ioc(1,R) ∪ Ioi R = Ioi 1. Subtracting the two convergent expressions yields a limit of zero; the final step transfers the limit to the original tail expression by eventual equality under the filter atTop.
why it matters
The result supplies the basic tail-control input for the half-line Sobolev decay argument that forces radial profiles to vanish at infinity. It directly supports the sibling ancientDecay_implies_tailFlux_vanish and thereby the coercivity hypothesis packaged in TailFluxVanishImpliesCoerciveHypothesis. Within the Recognition Science chain it closes the passage from uniform energy bounds on ancient solutions to vanishing flux at spatial infinity, consistent with the D = 3 spatial dimensions and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.