operatorPairing_of_decayFull
plain-language theorem explainer
AncientEnergyDecayFull on an RM2URadialProfile implies that rm2uOp(P) A r² is integrable over (1, ∞). Researchers on ancient Navier-Stokes solutions cite it to secure the operator pairing needed for Bet1 integrability. The tactic proof first verifies continuity of the integrand, then bounds each of the three decomposed terms by C² r^{-3} using the supplied decay rates, and concludes with the generic r^α-integrability lemma.
Claim. Let $P$ be an RM2URadialProfile. If $P$ satisfies the full ancient energy decay condition (with bounds $|A(r)|$ ≤ $C r^{-3/2}$, $|A'(r)|$ ≤ $C r^{-5/2}$, $|A''(r)|$ ≤ $C r^{-7/2}$ on $(1,∞)$ together with continuity of $A''$), then the function $r ↦$ rm2uOp$(P)(r) · A(r) · r²$ belongs to $L^1((1,∞))$.
background
The module RM2U Tail Flux Instantiation connects Galerkin-extracted ancient Navier-Stokes elements to the Bet1 integrability conditions required for the tail flux vanishing argument. AncientEnergyDecayFull extends the base decay structure by adding the second-derivative bound |A''(r)| ≤ C r^{-7/2} together with continuity of A'' on (1,∞). OperatorPairingIntegrable asserts that the product (rm2uOp P) A r² lies in L¹(1,∞).
proof idea
The proof unfolds OperatorPairingIntegrable, establishes positivity of 9 C² via sq_pos_of_pos, proves continuity of the integrand by composing the continuous functions A, A', A'' with the explicit form of rm2uOp, derives the pointwise bound |rm2uOp A r²| ≤ 9 C² r^{-3} by triangle inequality after algebraic rewriting of the three terms, and applies integrableOn_Ioi_of_rpow_decay with exponent -3.
why it matters
This result supplies the operator-pairing integrability hypothesis needed to reach Bet1 boundary integrability from the weighted L² moment and coercive bound. It is invoked inside the construction of GalerkinAncientElement. The declaration thereby instantiates the concrete link from finite-energy ancient elements to the algebraic Bet1 interface in the RM2U tail-flux chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.