SobolevH1HalfLineDecay
plain-language theorem explainer
The declaration defines the predicate SobolevH1HalfLineDecay(f, f') that packages the conditions for 1D Sobolev embedding on the half-line: square-integrability of f and f' on (1, ∞), differentiability with derivative f', and decay of f to zero at infinity. Navier-Stokes analysts working on ancient solutions and tail-flux vanishing cite this interface when closing energy estimates for radial profiles. The definition directly encodes the four classical conditions without additional lemmas.
Claim. Let $f, f' : (1,∞) → ℝ$. The predicate holds if $f, f' ∈ L^2(1,∞)$, $f$ is differentiable on $(1,∞)$ with derivative $f'$, and $f(r) → 0$ as $r → ∞$.
background
In the RM2U Tail Flux Instantiation module the predicate supplies the decay interface needed to pass from weighted L² moments on radial profiles A(r) to tail-flux vanishing. The module setting starts from Galerkin-extracted ancient Navier-Stokes elements whose energy inequality yields uniform L² bounds on gradients; projection onto the ℓ=2 spherical harmonic produces the radial function A(r) whose L² integrability on (1,∞) is inherited from Parseval on the sphere. The doc-comment records the classical Barbalat argument: the difference f(R) – f(r) is controlled by Cauchy-Schwarz on the derivative integral, the L² tail forces the sequence to be Cauchy, and L² integrability of f itself forces the limit to be zero.
proof idea
The definition is a direct conjunction of the four conditions: L² integrability of f on (1,∞), L² integrability of f' on (1,∞), pointwise differentiability via HasDerivAt, and the limit statement at infinity. No tactics or lemmas are applied; the body simply assembles the Prop that the downstream theorem sobolev_H1_half_line_decay then proves by the squared-function argument.
why it matters
The predicate is invoked inside TailFluxInstantiationCert to discharge the Sobolev decay hypothesis required for the self-consistent RM2U closure. That structure feeds the parent theorem rm2u_self_consistent_closure, which concludes RM2Closed from the weighted-moment and energy-forcing hypotheses. In the Recognition framework it supplies the concrete decay step that converts the energy inequality of ancient solutions into the integrable tail needed for Bet1 boundary-term control, closing the chain from Galerkin extraction to coercive L² bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.