integral_Ioi_radial_skew_identity
plain-language theorem explainer
Analysts studying Navier-Stokes regularity or Recognition Science tail estimates cite this identity to control skew-harmonic cancellations via integration by parts. It equates the integral over (1, ∞) of the radial skew operator applied to A with boundary contributions at 1 and infinity plus the squared-derivative integral. The proof proceeds by applying the general Ioi integration-by-parts lemma to u = -A and v = x² A', followed by algebraic sign adjustment on the cross term.
Claim. Let $A : (1,∞) → ℝ$ be twice differentiable with first derivative $A'$ and second derivative $A''$. Assume the functions $(-A(x))(2x A'(x) + x^2 A''(x))$ and $(-A'(x))(x^2 A'(x))$ are integrable over $(1,∞)$. Suppose the boundary expression $(-A(x) x^2 A'(x))$ tends to the finite limit $a'$ as $x → 1^+$ and to the finite limit $b'$ as $x → ∞$. Then ∫_{(1,∞)} (-A(x))(2x A'(x) + x^2 A''(x)) dx = b' - a' + ∫_{(1,∞)} (A'(x))^2 x^2 dx.
background
The module supplies integration-by-parts identities that support skew/self-adjoint cancellations and harmonic/affine tail bookkeeping for Navier-Stokes analysis inside Recognition Science. The local setting restricts attention to the half-line (1, ∞) so that boundary terms appear only at the lower endpoint and at infinity, matching the TeX remark that a bad tail violates zero-skew at infinity. Upstream results supply the product rule for x² A' (via the sibling hasDerivAt_rsq_mul) together with basic negation and multiplication identities from the Foundation arithmetic and integer modules.
proof idea
The proof first constructs HasDerivAt witnesses for u = -A and for v = x² A' by negating the given derivative of A and invoking hasDerivAt_rsq_mul on the second derivative of A. It then calls the general lemma MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul with these witnesses and the supplied integrability and Tendsto hypotheses. The resulting identity is rearranged by pulling the outer negation through the integral and applying pointwise algebra A' · (x² A') = (A')² x² to obtain the positive squared term.
why it matters
The lemma supplies a clean radial integration-by-parts identity that directly implements the first analytic step listed in the module doc-comment for navier-dec-12-rewrite.tex. It therefore sits inside the Recognition Science forcing chain as a tool for controlling skew terms that arise once D = 3 and the eight-tick octave are fixed. No downstream uses are recorded, so the declaration remains a foundational building block whose closure would be a vanishing-boundary theorem for admissible tails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.