AncientEnergyDecayFull
plain-language theorem explainer
AncientEnergyDecayFull extends the base energy decay of an RM2URadialProfile by adding a second-derivative bound |A''(r)| ≤ C r^{-7/2} together with continuity of A'' on (1,∞). Navier-Stokes analysts working on ancient solutions cite it to close integrability of the operator pairing rm2uOp(P) · A · r². The declaration is a structure extension that packages the strengthened decay directly from the radial ODE without additional lemmas.
Claim. Let $P$ be an RM2URadialProfile with coefficient functions $A$, $A'$, $A''$. The structure AncientEnergyDecayFull$(P)$ consists of the base decay $|A(r)| ≤ C r^{-3/2}$ and $|A'(r)| ≤ C r^{-5/2}$ for $r > 1$, extended by the second-derivative bound $|A''(r)| ≤ C r^{-7/2}$ for $r > 1$ and continuity of $A''$ on $(1,∞)$.
background
The module connects Galerkin-extracted ancient Navier-Stokes elements to the Bet1 integrability conditions required for tail-flux vanishing. An RM2URadialProfile abstracts the ℓ=2 radial coefficient $A(r)$ of a fixed-time velocity slice together with its first and second derivatives satisfying the chain-rule relations HasDerivAt. AncientEnergyDecay supplies the base decay $|A(r)| ≤ C r^{-3/2}$ and $|A'(r)| ≤ C r^{-5/2}$ that follows from finite energy via Parseval projection onto the sphere. The extension adjoins the second-derivative bound whose rate is forced by the radial ODE $A'' = -2A'/r + 6A/r² +$ forcing term, as stated in the sibling doc-comment.
proof idea
This is a structure definition that extends AncientEnergyDecay P by adjoining the second-derivative decay bound and the continuity statement for A''. No tactics or lemmas are applied; the bounds are postulated as part of the hypothesis package for downstream integrability arguments.
why it matters
It supplies the strengthened decay hypothesis needed for operatorPairing_of_decayFull, which establishes that rm2uOp(P) · A · r² is integrable on (1,∞). This integrability closes the chain from GalerkinAncientElement to the Bet1 boundary term condition. The construction sits inside the RM2U tail flux instantiation that converts uniform energy bounds into the coercivity hypothesis required for ancient solution classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.