bet1_boundaryTerm_integrable_of_L2_mul_r
plain-language theorem explainer
If a radial profile A and its derivative A' both lie in the weighted L² space with weight r² on (1,∞), then the product forming the boundary flux term (-A)·(A'·r²) is integrable on that interval. Navier-Stokes workers applying the RM2U ansatz cite the result to control the tail contribution in the non-parasitism gate. The argument lifts the two given integrability hypotheses to L² membership on the restricted measure, invokes the L² product theorem, and rewrites the integrand by a pointwise ring identity.
Claim. Let $P$ be an RM2URadialProfile. If $A(r)r$ and $A'(r)r$ both belong to $L^2((1,∞))$, then the function $r↦(-A(r))·(A'(r)·r^2)$ is integrable on $(1,∞)$.
background
The RM2U.NonParasitism module isolates the single hard non-parasitism statement required to pass from the RM2U ansatz to the RM2 pipeline; the module doc-comment defines this as the requirement that the tail-flux boundary term vanishes at infinity for the relevant ℓ=2 coefficient. An RM2URadialProfile supplies a function A together with its derivative A' and the continuity hypotheses needed on (1,∞). IntegrableOn f s μ asserts that the restriction of f to s is integrable with respect to the measure μ; here the measure is Lebesgue volume restricted to the half-line (1,∞). The present theorem supplies the integrability of the concrete boundary integrand B(r)=(-A(r))·(A'(r)·r²) once the two weighted L² conditions are given.
proof idea
The tactic proof first restricts to the measure μ=volume.restrict(Ioi 1). It obtains continuity of A and A' on the interval from the profile hypotheses, deduces a.e. strong measurability of the scaled maps r↦(-A r)·r and r↦(A' r)·r, then applies memLp_two_iff_integrable_sq to convert the supplied weighted L² hypotheses into L²(μ) membership. MemLp.integrable_mul (the L²-L² case of Hölder) yields integrability of the product; a final congr step rewrites the integrand pointwise into the desired boundary term via the ring identity.
why it matters
The lemma is the core integrability engine inside the non-parasitism gate of the RM2U reduction. It is invoked directly by the downstream wrapper bet1_boundaryTerm_integrable_of_A2r_and_coercive, which adds the coercive L² bound hypothesis. In the Recognition Science setting the result helps close the tail-flux vanishing condition that converts the RM2U ansatz into a clean RM2 pipeline; the module doc-comment identifies non-parasitism as the single hard statement that must be isolated as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.