Finite-Moment Elimination

Abstract

An endpoint delta jet cancels finitely many centered moments without changing the Weil correlation pairing.

Theorem 1.1 (Finite moment elimination by an endpoint delta jet).

$$\begin{array}{r}\forall L:\mathrm{Real}\left(\right),K:\mathrm{Natural}\left(\right),epsilon:\mathrm{SignedMeasure}\left(\mathrm{Real}\left(\right)\right),\\ hpos:\mathrm{restrict}\left(\mathrm{posPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),\mathrm{Icc}\left(0,2\cdot L\right)\right)=\mathrm{posPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),hneg:\mathrm{restrict}\left(\mathrm{negPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),\mathrm{Icc}\left(0,2\cdot L\right)\right)=\mathrm{negPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right),\\ f,h:\mathrm{Real}\left(\right)\to \mathrm{Complex}\left(\right),hfSmooth:\mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),f\right),\\ hhSmooth:\mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),h\right),hfCompact:\mathrm{HasCompactSupport}\left(f\right),\\ hhCompact:\mathrm{HasCompactSupport}\left(h\right),hfSupport:\mathrm{tsupport}\left(f\right)\subseteq \mathrm{Ioo}\left(-L,L\right),\\ hhSupport:\mathrm{tsupport}\left(h\right)\subseteq \mathrm{Ioo}\left(-L,L\right)\Rightarrow \\ \mathrm{let}b:=2\cdot L,\\ \mathrm{let}moment:=\mathrm{lambda}\left(j,\mathrm{signedIntegral}\left(u,\mathrm{pow}\left(u-b,j\right),epsilon\right)\right),\\ \mathrm{let}measureDistribution:\mathrm{TemperedDistribution}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right):=\mathrm{toTemperedDistribution}\left(\mathrm{posPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right)\right)-\mathrm{toTemperedDistribution}\left(\mathrm{negPart}\left(\mathrm{toJordanDecomposition}\left(epsilon\right)\right)\right),\\ \mathrm{let}correction:\mathrm{TemperedDistribution}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right):=\mathrm{sum}\left(j,\mathrm{range}\left(K+1\right),\mathrm{smul}\left(\mathrm{complex}\left(\frac{\mathrm{pow}\left(-1,j+1\right)\cdot moment\left(j\right)}{\mathrm{factorial}\left(j\right)}\right),\mathrm{iterate}\left(\mathrm{temperedDerivative}\left(\mathrm{Complex}\left(\right)\right),j,\mathrm{delta}\left(b\right)\right)\right)\right),\\ \mathrm{let}correctedDistribution:=measureDistribution+correction,\\ \mathrm{let}correlation:=\mathrm{weilTest}\left(f,h\right),\\ \mathrm{let}hcorrelationCompact:\mathrm{HasCompactSupport}\left(correlation\right):=\mathrm{weilTestHasCompactSupport}\left(hfCompact,hhCompact\right),\\ \mathrm{let}hcorrelationSmooth:\mathrm{ContDiff}\left(\mathrm{Real}\left(\right),\mathrm{infinity}\left(\right),correlation\right):=\mathrm{weilTestContDiff}\left(hfSmooth,hhSmooth,hhCompact\right),\\ \mathrm{let}correlationTest:=\mathrm{toSchwartzMap}\left(correlation,hcorrelationCompact,hcorrelationSmooth\right),\\ \forall test\in \mathrm{SchwartzMap}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right),correctedDistribution\left(test\right)=\mathrm{signedIntegral}\left(u,test\left(u\right),epsilon\right)+\mathrm{sum}\left(j,\mathrm{range}\left(K+1\right),\mathrm{complex}\left(\frac{\mathrm{pow}\left(-1,j+1\right)\cdot moment\left(j\right)}{\mathrm{factorial}\left(j\right)}\right)\cdot \mathrm{pow}\left(\mathrm{complex}\left(-1\right),j\right)\cdot \mathrm{iterate}\left(\mathrm{schwartzDerivative}\left(\mathrm{Complex}\left(\right),\mathrm{Complex}\left(\right)\right),j,test\right)\left(b\right)\right)\wedge \forall p\in \mathrm{Polynomial}\left(\mathrm{Real}\left(\right)\right),\mathrm{natDegree}\left(p\right)\le K\Rightarrow \mathrm{signedIntegral}\left(u,\mathrm{eval}\left(p,u\right),epsilon\right)+\mathrm{sum}\left(j,\mathrm{range}\left(K+1\right),\frac{\mathrm{pow}\left(-1,j+1\right)\cdot moment\left(j\right)}{\mathrm{factorial}\left(j\right)}\cdot \mathrm{pow}\left(-1,j\right)\cdot \mathrm{eval}\left(\mathrm{iterate}\left(\mathrm{polynomialDerivative}\left(\mathrm{Real}\left(\right)\right),j,p\right),b\right)\right)=0\wedge correctedDistribution\left(correlationTest\right)=measureDistribution\left(correlationTest\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The signed measure is embedded canonically through its Jordan parts. A finite Taylor expansion proves polynomial annihilation, while strict doubled-window support makes every endpoint jet vanish on the constructed Weil correlation.

References

• Truth anchor: D5/S3/Weil/TestFunctions/FiniteMomentElimination.finite_moment_elimination