External-Support Invisibility

Abstract

A compactly supported Weil correlation is unchanged by adding a tempered distribution whose distributional support lies outside its doubled window.

Theorem 1.1 (External support is invisible to local Weil correlations).

$$\begin{array}{r}\forall L:\mathrm{Real}\left(\right),weilSource,kappa:\mathrm{TemperedDistribution}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right),\\ hkappa:\mathrm{dsupport}\left(kappa\right)\subseteq \mathrm{compl}\left(\mathrm{Ioo}\left(-2L,2\cdot L\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}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{contDiffConvolutionRight}\left(\mathrm{hasCompactSupportTilde}\left(hhCompact\right),hfSmooth,\mathrm{contDiffTilde}\left(hhSmooth\right)\right),\\ \mathrm{let}correlationTest:=\mathrm{toSchwartzMap}\left(correlation,hcorrelationCompact,hcorrelationSmooth\right),\\ \mathrm{add}\left(weilSource,kappa\right)\left(correlationTest\right)=weilSource\left(correlationTest\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The canonical Weil correlation is constructed from the two supplied smooth compact tests. Its strict doubled-window support permits a finite smooth partition-of-unity decomposition into neighborhoods where the added tempered distribution vanishes.

References

• Truth anchor: D5/S3/Weil/TestFunctions/ExternalSupportInvisibility.external_support_invisibility