ancientDecay_implies_A2_integrable
plain-language theorem explainer
Ancient energy decay for the ℓ=2 radial profile implies square-integrability of A over (1, ∞). Workers on ancient Navier-Stokes solutions and the RM2U tail-flux closure cite this step. The proof invokes the general rpow-decay integrability lemma and squares the supplied C r^{-3/2} bound to obtain an r^{-3} majorant whose integral converges.
Claim. Let P be a radial profile for the ℓ=2 mode. If |A(r)| ≤ C r^{-3/2} for all r > 1 with C > 0, then ∫_{(1,∞)} A(r)^2 dr < ∞.
background
The module instantiates tail-flux vanishing for ancient Navier-Stokes elements extracted by Galerkin diagonal convergence. It connects uniform energy bounds ∫ |∇u|^2 ≤ C to integrability conditions on the projected radial profile A(r). AncientEnergyDecay encodes the finite-energy decay at spatial infinity: |A(r)| ≤ C r^{-3/2} (and |A'(r)| ≤ C r^{-5/2}) for r ≥ 1. The module docstring states that this decay follows from the velocity field vanishing at infinity, standard for NS, and yields A(r)^2 = O(r^{-1}) which is integrable on (1,∞).
proof idea
One-line wrapper that applies integrableOn_Ioi_of_rpow_decay with exponent -3. The tactic supplies the strict inequality -3 < -1, positivity of C, continuity of A, and a short calculation: (C r^{-3/2})^2 = C^2 r^{-3} after using abs_of_nonneg and mul_pow. The rpow_mul and norm_num steps confirm the exponent.
why it matters
This supplies the A² integrability half of CoerciveL2Bound. It is invoked directly by ancientDecay_implies_coercive to produce the full coercive hypothesis needed for bet1_boundaryTerm_integrable_of_A2r_and_coercive. The result closes one link in the chain from Galerkin energy bounds through Parseval on S² to the tail-flux vanishing condition for ancient solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.