bet1_of_bet1Alt
plain-language theorem explainer
The alternate Bet-1 boundary integrability hypothesis on an RM2U radial profile implies the original Bet-1 hypothesis. Navier-Stokes analysts working on the RM2U closure cite this implication when moving between the coercive pairing formulation and direct derivative integrability. The proof constructs the restricted measure on (1,∞), verifies integrability of the rewritten RHS by subtraction of the supplied integrable terms, establishes an almost-everywhere equality via the boundary-term derivative identity, and transfers integrability by congr
Claim. Let $P$ be an RM2U radial profile. If the alternate Bet-1 hypothesis holds, i.e., $(-A)(A'r^2)$ is integrable on $(1,∞)$, the RM2U operator pairing is integrable on $(1,∞)$, and the coercive $L^2$ bounds on $A$ and $A'$ hold, then the original Bet-1 hypothesis holds: both $(-A)(A'r^2)$ and its derivative integrand $(-A')(A'r^2)+(-A)(A''r^2+A'·2r)$ are integrable on $(1,∞)$.
background
In the RM2U.NonParasitism module the single hard gate is non-parasitism, expressed as vanishing of the tail-flux boundary term at infinity for the ℓ=2 coefficient. The original Bet-1 hypothesis requires integrability on (1,∞) of both the boundary integrand (-A)(A'r²) and the formal derivative expression (-A')(A'r²)+(-A)(A''r²+A'·2r). The alternate version keeps the first integrability but replaces the second by integrability of the RM2U operator pairing together with coercive L² control on A and A' (CoerciveL2Bound P).
proof idea
The tactic proof refines the structure to retain the shared boundary integrability. It defines the restricted measure μ on (1,∞), extracts integrability of the pairing, of A², and of (A')²r² from the alternate hypothesis, then closes the rewritten RHS under subtraction. An almost-everywhere equality is obtained by applying bet1_boundaryTerm_deriv_integrand_eq pointwise on x>1 (using lt_trans for x≠0), after which congruence transfers integrability to the original derivative integrand.
why it matters
The implication is used by bet1_original_for_galerkin to convert the Galerkin-supplied alternate hypothesis into the original Bet-1 interface, and by tailFlux_vanishes_from_weighted_moment to close the weighted-moment route to TailFluxVanish. It therefore bridges the coercive formulation and the direct integrability statement needed for non-parasitism in the RM2U closure. The result touches the open question of discharging the full non-parasitism hypothesis from the Galerkin ancient element.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.