zeroSkewAtInfinity_of_integrable
plain-language theorem explainer
This lemma shows that if the radial flux term (-A(x)) * (A'(x) * x^2) and its derivative are integrable on (1, ∞), then the flux tends to zero at infinity. Analysts formalizing energy identities for radial Navier-Stokes profiles cite it to justify vanishing boundary terms over unbounded domains. The argument first verifies the derivative of the flux via the product rule on the given differentiability hypotheses, then invokes the standard calculus result that an integrable function with integrable derivative tends to zero at infinity.
Claim. Assume $A:(1,∞)→ℝ$ is twice differentiable with derivatives $A'$ and $A''$. If both $f(x)=(-A(x))⋅(A'(x)⋅x^2)$ and $f'(x)$ are integrable on $(1,∞)$, then $lim_{x→∞}f(x)=0$.
background
The Navier–Stokes skew/harmonic tail gate module formalizes two analytic steps that recur in navier-dec-12-rewrite.tex: skew/self-adjoint cancellations from integration by parts (no bad boundary term) and harmonic/affine tail mode bookkeeping, where the only obstruction is a boundary term at infinity. The flux term (-A) * (A' * r^2) appears directly in radial energy identities; the module leaves the hard tail-decay implication as an explicit Tendsto hypothesis, matching the TeX language of bad tails violating zero-skew at infinity.
proof idea
The proof first builds a local HasDerivAt statement for the flux function by applying the product rule: negation of the outer factor, the inner product A' * x^2 via hasDerivAt_rpow_two, and the outer multiplication. It then applies MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi directly to the supplied integrability hypotheses on the flux and its derivative.
why it matters
This lemma is invoked by tailFluxVanish_of_integrable and integral_rm2uOp_mul_energy_identity in the RM2U EnergyIdentity module. The latter supplies the precise Lean analogue of the integration-by-parts step inside TeX Remark rem:Ab-energy-identity on a finite window [a,R]. It closes the boundary term for the RM2U operator and thereby supports the skew cancellations required for Navier-Stokes energy estimates in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.