LogCriticalMomentFinite
plain-language theorem explainer
LogCriticalMomentFinite encodes the integrability condition A(r)/r ∈ L¹((1,∞), dr) for the radial coefficient in the RM2U tail obstruction. Navier-Stokes analysts working on the simplified 1D radial model would cite it when checking closure under coercive bounds. The definition is a direct abbreviation that invokes Mathlib's IntegrableOn predicate on the half-line with Lebesgue volume.
Claim. A radial function $A : ℝ → ℝ$ has finite log-critical moment when $A(r)/r$ is integrable over the interval $(1, ∞)$ with respect to Lebesgue measure, i.e., $∫_{(1,∞)} |A(r)/r| dr < ∞$.
background
The RM2U.Core module supplies the Lean specification for the RM2U tail/tightness gate, reducing the problem to a 1D radial coefficient A(r) for r ≥ 1 at fixed time and direction parameter b. The manuscript expresses the obstruction via the boundary/tail-flux term (-A(r)) · (A'(r) · r²) as r → ∞. This definition isolates the log-critical shell moment as the concrete integrability requirement A(r)/r ∈ L¹((1,∞), dr). Upstream results supply auxiliary A symbols (active edge count, actualization operator, volume) that appear in the broader framework but are not invoked inside this definition.
proof idea
The declaration is a one-line definition that directly applies the IntegrableOn predicate to the function fun r => A r / r over Set.Ioi 1 with respect to volume measure.
why it matters
It supplies the base predicate for RM2Closed in the RM2Closure sibling module, which encodes the manuscript's one-line Cauchy-Schwarz argument that L² control on A implies the log-critical moment is finite. The definition therefore closes the simplified radial model of the RM2 obstruction and feeds the coerciveL2Bound implication theorem. It sits inside the Navier-Stokes reduction that reuses SkewHarmGate identities from the parent EnergyIdentity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.