integral_radial_skew_identity
plain-language theorem explainer
The lemma delivers an exact integration-by-parts identity converting the radial skew operator integral of A into explicit boundary terms at 1 and R plus the positive quadratic integral of (A')² x². Analysts deriving energy estimates for the Navier-Stokes equations in spherical coordinates would cite it to absorb the skew term without remainder. The proof applies Mathlib's interval integration-by-parts lemma after constructing the required HasDerivAt facts for -A and x² A' via the sibling hasDerivAt_rsq_mul.
Claim. Let $A : [1,R] → ℝ$ with $R ≥ 1$ be twice differentiable, with $A'$ and $A''$ its first and second derivatives. Assume the relevant first-derivative and weighted-second-derivative combinations are interval-integrable on $[1,R]$. Then
background
The SkewHarmGate module supplies integration-by-parts identities that realize skew/self-adjoint cancellations for radial profiles, as needed for the analytic steps in navier-dec-12-rewrite.tex. Here A is a radial function, A' its derivative, and the operator -(A'' + (2/x)A') is the radial part of the skew form. The hypotheses guarantee differentiability on the compact interval uIcc 1 R together with integrability of A' and of the combination (2x A' + x² A'').
proof idea
The proof first builds HasDerivAt facts hu for -A and hv for x² A' (the latter via the sibling hasDerivAt_rsq_mul). It invokes intervalIntegral.integral_mul_deriv_eq_deriv_mul to obtain the parts formula. A congruence step rewrites the integrand to the target skew form, after which a calc block adjusts signs on the boundary terms and converts the remaining integral of (-A') (x² A') into the positive ∫ (A')² x² term.
why it matters
This identity is the direct algebraic engine for the generalized lemma integral_radial_skew_identity_from that relaxes the lower limit. It supplies the finite-radius skew cancellation step required by the module's stated purpose: 'support the two analytic steps that show up repeatedly in navier-dec-12-rewrite.tex' for skew/self-adjoint cancellations. In the Recognition framework it furnishes the exact radial identity before any tail-decay argument at infinity is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.