Smooth External Moment Elimination

Abstract

An even smooth correction supported outside a finite interval cancels every prescribed even moment through a fixed order.

Theorem 1.1 (Smooth exterior cancellation of finitely many even moments).

$$\forall L\in \mathrm{Real}\left(\right),K\in \mathrm{Natural}\left(\right),epsilon\in \mathrm{SignedMeasure}\left(\mathrm{Real}\left(\right)\right),\left(\mathrm{restrict}\left(\mathrm{posPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),\mathrm{Icc}\left(-2L,2\cdot L\right)\right)=\mathrm{posPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right)\wedge \mathrm{restrict}\left(\mathrm{negPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),\mathrm{Icc}\left(-2L,2\cdot L\right)\right)=\mathrm{negPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right)\right)\Rightarrow \left(\exists kappa\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{Even}\left(kappa\right)\wedge \left(\mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),kappa\right)\wedge \left(\mathrm{HasCompactSupport}\left(kappa\right)\wedge \left(\mathrm{tsupport}\left(kappa\right)\subseteq \mathrm{compl}\left(\mathrm{Icc}\left(-2L,2\cdot L\right)\right)\wedge \left(\forall j\in \mathrm{Natural}\left(\right),j\le K\Rightarrow \mathrm{signedIntegral}\left(u,\mathrm{pow}\left(u,2\cdot j\right),epsilon\right)+\mathrm{integral}\left(u,\mathrm{pow}\left(u,2\cdot j\right)\cdot kappa\left(u\right),\mathrm{volume}\left(\right)\right)=0\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/SmoothExternalMomentElimination.smooth_external_finite_moment_elimination (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reflected pairs of even derivatives of one compact bump form a lower triangular moment family. Integration by parts makes its diagonal nonzero, so the inverse finite moment matrix supplies the displayed even correction without entering the source interval.

References

• Truth anchor: D5/S3/Weil/TestFunctions/SmoothExternalMomentElimination.smooth_external_finite_moment_elimination