Spectral Concentration Positivity

Abstract

A supremal band-concentration rate gives an explicit lower bound for a spectrally weighted quadratic form and a strict positivity certificate.

Theorem 1.1 (Spectral concentration positivity certificate).

$$\forall Test\in Type,supportedIn\in \mathrm{Real}\left(\right)\to \left(Test\to Prop\right),spatialMass\in Test\to \mathrm{Real}\left(\right),spectralDensity\in Test\to \left(\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right)\right),M\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),B\in \mathrm{Set}\left(\mathrm{Real}\left(\right)\right),L\in \mathrm{Real}\left(\right),a\in \mathrm{Real}\left(\right),b\in \mathrm{Real}\left(\right),\left(\mathrm{Zero}\left(Test\right)\wedge \left(\mathrm{MeasurableSet}\left(B\right)\wedge \left(0<a\wedge \left(0\le b\wedge \left(\left(\forall xi\in \mathrm{Real}\left(\right),\left(\neg xi\in B\right)\Rightarrow a\le \mathrm{apply}\left(M,xi\right)\right)\wedge \left(\left(\forall xi\in \mathrm{Real}\left(\right),xi\in B\Rightarrow \mathrm{neg}\left(b\right)\le \mathrm{apply}\left(M,xi\right)\right)\wedge \left(\left(\forall f\in Test,\mathrm{Integrable}\left(\mathrm{apply}\left(spectralDensity,f\right)\right)\right)\wedge \left(\left(\forall f\in Test,\mathrm{Integrable}\left(xi:\mathrm{Real}\left(\right)\mapsto \mathrm{mul}\left(\mathrm{apply}\left(M,xi\right),\mathrm{applyTwo}\left(spectralDensity,f,xi\right)\right)\right)\right)\wedge \left(\left(\forall f\in Test,xi\in \mathrm{Real}\left(\right),0\le \mathrm{applyTwo}\left(spectralDensity,f,xi\right)\right)\wedge \left(\left(\forall f\in Test,\mathrm{mul}\left(\mathrm{div}\left(1,\mathrm{mul}\left(2,\mathrm{pi}\left(\right)\right)\right),\mathrm{integral}\left(\mathrm{Real}\left(\right),xi:\mathrm{Real}\left(\right)\mapsto \mathrm{applyTwo}\left(spectralDensity,f,xi\right)\right)\right)=\mathrm{apply}\left(spatialMass,f\right)\right)\wedge \left(\left(\forall xi\in \mathrm{Real}\left(\right),\mathrm{applyTwo}\left(spectralDensity,0,xi\right)=0\right)\wedge \left(\forall f\in Test,f\ne 0\Rightarrow 0<\mathrm{apply}\left(spatialMass,f\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}concentrationRatios=\left\{\exists f\in Test,f\ne 0\wedge \left(\mathrm{applyTwo}\left(supportedIn,L,f\right)\wedge ratio=\mathrm{div}\left(\mathrm{mul}\left(\mathrm{div}\left(1,\mathrm{mul}\left(2,\mathrm{pi}\left(\right)\right)\right),\mathrm{integralOn}\left(B,xi:\mathrm{Real}\left(\right)\mapsto \mathrm{applyTwo}\left(spectralDensity,f,xi\right)\right)\right),\mathrm{apply}\left(spatialMass,f\right)\right)\right)\mid ratio\in \mathrm{Real}\left(\right)\right\},\mathrm{let}concentration=\mathrm{sSup}\left(concentrationRatios\right),\mathrm{let}quadraticForm=f:Test\mapsto \mathrm{mul}\left(\mathrm{div}\left(1,\mathrm{mul}\left(2,\mathrm{pi}\left(\right)\right)\right),\mathrm{integral}\left(\mathrm{Real}\left(\right),xi:\mathrm{Real}\left(\right)\mapsto \mathrm{mul}\left(\mathrm{apply}\left(M,xi\right),\mathrm{applyTwo}\left(spectralDensity,f,xi\right)\right)\right)\right),\left(\forall f\in Test,\mathrm{applyTwo}\left(supportedIn,L,f\right)\Rightarrow \mathrm{mul}\left(\mathrm{sub}\left(a,\mathrm{mul}\left(\mathrm{add}\left(a,b\right),concentration\right)\right),\mathrm{apply}\left(spatialMass,f\right)\right)\le \mathrm{apply}\left(quadraticForm,f\right)\right)\wedge \left(concentration<\mathrm{div}\left(a,\mathrm{add}\left(a,b\right)\right)\Rightarrow \left(\forall f\in Test,\left(f\ne 0\wedge \mathrm{applyTwo}\left(supportedIn,L,f\right)\right)\Rightarrow 0<\mathrm{apply}\left(quadraticForm,f\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/SpectralConcentrationPositivity.spectral_concentration_positivity_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The ratio set is built from the nonzero tests supported in the chosen spatial window. Its supremum is the concentration rate, while the weighted spectral integral is the quadratic form.

Nonnegative spectral density and Plancherel normalization bound every band ratio by one. Splitting the weighted integral over the band and its complement yields the displayed gap; the strict threshold then makes that gap positive on every supported nonzero test.

References

• Truth anchor: D5/S3/Weil/ZetaBridge/SpectralConcentrationPositivity.spectral_concentration_positivity_certificate