sobolev_H1_half_line_decay
plain-language theorem explainer
If a real-valued function and its derivative are both square-integrable on the half-line (1, ∞), then the function tends to zero at infinity. Navier-Stokes analysts working on ancient solutions cite the result to control tail fluxes after radial projection of Galerkin limits. The proof reduces the claim to the library decay lemma applied to f squared once Hölder confirms integrability of the product 2f f'.
Claim. Let $f, f' : ℝ → ℝ$. If $∫_{(1,∞)} |f(r)|^2 dr < ∞$, $∫_{(1,∞)} |f'(r)|^2 dr < ∞$, and $f$ is differentiable on $(1,∞)$ with derivative $f'$, then $f(r) → 0$ as $r → ∞$.
background
SobolevH1HalfLineDecay encodes the classical one-dimensional Sobolev embedding H¹(1,∞) ↪ C₀(1,∞): square-integrability of both the function and its derivative on the half-line, together with pointwise differentiability, forces the function to vanish at infinity. The module TailFluxInstantiation places this embedding inside the chain that converts the uniform energy bound from Galerkin extraction into the weighted L² moment and tail-flux vanishing needed for the coercive hypothesis on ancient Navier-Stokes elements.
proof idea
The tactic proof restricts Lebesgue measure to Ioi 1, verifies continuity and measurability of f, confirms both f and f' lie in L²(μ), shows that the derivative of f² equals 2f f' and is integrable by the L² product rule, then invokes tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi on f². The final step passes to the absolute value via the continuous square-root map to obtain the required limit.
why it matters
The theorem supplies the sobolev_decay component of tailFluxInstantiationCert, which discharges TailFluxVanishImpliesCoerciveHypothesis for concrete ancient elements extracted by Galerkin diagonal convergence. It thereby closes the loop from the energy inequality through the radial projection A(r) to the Bet1 integrability conditions listed in the module chain. In the Recognition Science framework this supplies the spatial-decay step that feeds the energy-conservation domain certificate into the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.