Approximate Complementary Concentration

Abstract

Residual spectral energy controls the mass away from Fourier near-zeros.

Theorem 1.1 (Residual spectral mass concentrates near Fourier zeros).

$$\begin{array}{r}\forall mu:\mathrm{Measure}(\mathbb{R}),F:\mathbb{R}\to \mathbb{C},\\ epsilon:\mathrm{ENNReal}(),delta:NNReal,\\ \mathrm{AEMeasurable}(F,mu)\wedge 0<delta\wedge \mathrm{lintegral}(mu,(xi:\mathbb{R}\mapsto \mathrm{enorm}(\mathrm{apply}(F,xi){)}^2))=epsilon\Rightarrow \\ \mathrm{measure}(mu,\left\{\mathrm{toENNReal}(delta)\le \mathrm{enorm}(\mathrm{apply}(F,xi))\mid xi\in \mathbb{R}\right\})\le \frac{epsilon}{\mathrm{toENNReal}(delta{)}^2}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/ApproximateComplementaryConcentration.approximate_complementary_concentration (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a positive Borel measure carry the residual spectrum and let a measurable complex function be the Fourier transform of the window test.

If its squared modulus has residual energy epsilon, Markov’s inequality bounds the mass where the modulus exceeds a positive finite threshold delta by epsilon divided by delta squared.

References

• Truth anchor: D5/S3/Weil/Budget/ApproximateComplementaryConcentration.approximate_complementary_concentration