rm2Closed_of_coerciveL2Bound
plain-language theorem explainer
Coercive L2 control on the radial profile A forces the log-critical shell moment to be finite. Modelers closing the RM2U system for ancient Navier-Stokes elements cite this to obtain RM2Closed from an energy-type bound. The argument reduces to a domination inequality that lets the L2 integrability of A absorb the 1/r weight via an elementary quadratic comparison.
Claim. If the radial profile $A$ satisfies the coercive $L^2$ bound on $(1,∞)$, then the log-critical moment is finite: $∫_1^∞ |A(r)|/r dr < ∞$.
background
The module supplies the classical closure steps for the RM2U model. RM2Closed is defined as the finiteness of the log-critical moment of the coefficient A. CoerciveL2Bound encodes L2 integrability of A over (1,∞). The setting follows the manuscript argument that L2 control on A implies L1 control on A/r because 1/r lies in L2 on that interval.
proof idea
The proof extracts L2 integrability of A from the coercive hypothesis and records integrability of r^{-2} on (1,∞) via integrableOn_Ioi_rpow_of_lt. It forms the dominating integrable function A^2 + r^{-2}, establishes continuity of A/r, and deduces a.e. measurability. The key step applies two_mul_le_add_sq to obtain the pointwise bound |A|/r ≤ A^2 + r^{-2} a.e., using nlinarith for the coefficient comparison and real-power identities for the exponents.
why it matters
This result supplies the base implication that feeds rm2_closed_for_galerkin in BetInstantiation and the Bet3 and non-parasitism closures in NonParasitism. It encodes the manuscript's one-line Cauchy-Schwarz step that turns coercive L2 control into RM2 closure. The lemma supports the full RM2U pipeline for ancient elements by linking the energy identity to the moment finiteness. It leaves open the replacement of the interface hypothesis CoerciveImpliesRM2Hypothesis by a direct compactness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.