integral_radial_skew_identity_from
plain-language theorem explainer
This lemma delivers the finite-interval integration-by-parts identity for the radial skew operator on [a, R] with a > 0. It equates the integral of (-A'' - (2/x)A') A x^2 to the explicit boundary terms -A(R)R^2 A'(R) + A(a)a^2 A'(a) plus the integral of (A')^2 x^2. Analysts deriving energy identities for radial Navier-Stokes profiles cite it to control boundary contributions on bounded domains. The proof applies the general interval integration-by-parts lemma after constructing derivative hypotheses for -A and x^2 A' and rewriting the integrand
Claim. Assume $a ≤ R$ and $0 < a$. Let $A$ be twice differentiable on the closed interval $[a,R]$ with $A'$ and the indicated combination of $A'$ and $A''$ interval-integrable. Then $$∫_a^R (-A''(x) - (2/x)A'(x)) A(x) x^2 dx = -A(R) R^2 A'(R) + A(a) a^2 A'(a) + ∫_a^R (A'(x))^2 x^2 dx.$$
background
The NavierStokes.SkewHarmGate module formalizes skew/self-adjoint cancellations from integration by parts and harmonic/affine tail bookkeeping, matching the analytic steps in navier-dec-12-rewrite.tex. The radial skew expression -(A'' + (2/x)A') arises as the divergence-form operator in spherical coordinates; the lemma isolates its boundary terms on any finite interval [a,R] with a > 0. Upstream results supply the product-rule derivative hasDerivAt_rsq_mul for v = x^2 A' and the Mathlib interval integration-by-parts theorem; the module doc notes that the hard tail-decay step (boundary term vanishes at infinity) is left as an explicit Tendsto hypothesis.
proof idea
Construct HasDerivAt hypotheses for u = -A (by negation of hA) and for v = x^2 A' (by hasDerivAt_rsq_mul applied to hA'). Negate the given integrability of A' to obtain integrability of u'. Apply intervalIntegral.integral_mul_deriv_eq_deriv_mul. Rewrite the resulting integrand to the target skew form via intervalIntegral.integral_congr, field_simp and ring. Finish with a calc block that tracks signs explicitly, using neg_mul and integral_neg to convert the cross term into the positive ∫ (A')^2 x^2 integral.
why it matters
The lemma supplies the calculus core for the downstream theorem integral_rm2uOp_mul_energy_identity in NavierStokes.RM2U.EnergyIdentity, the precise Lean analogue of the integration-by-parts step in TeX Remark rem:Ab-energy-identity. It advances the skew-cancellation program of the module doc for radial Navier-Stokes profiles and supports the fluid bridge in ClassicalBridge.Fluids.LNAL. In the Recognition Science setting it provides rigorous control over radial integrals without invoking full PDE content; the open question it leaves is the separate vanishing of boundary terms at infinity under suitable decay.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.