Support Rayleigh Monotonicity

Abstract

A support-window enlargement expands the normalized Weil test class and cannot increase the lowest Rayleigh value of a window-invariant quadratic cost.

Theorem 1.1 (The lowest Rayleigh value is antitone under support enlargement).

$$\begin{array}{r}\forall q:\mathbb{R}\to \mathcal{W}\to \mathbb{R},L_1,L_2\in \mathbb{R},\\ \mathrm{let}{R}_1=\{q\left(L_1,f\right)\mid f\in \mathcal{W},\mathrm{tsupport}\left(f\right)\subseteq \mathrm{Ioo}\left(-L_1,L_1\right)\wedge l2Mass\left(f\right)=1\},\\ R_2=\{q\left(L_2,f\right)\mid f\in \mathcal{W},\mathrm{tsupport}\left(f\right)\subseteq \mathrm{Ioo}\left(-L_2,L_2\right)\wedge l2Mass\left(f\right)=1\},\\ L_1<L_2\wedge \forall f\in \mathcal{W},\mathrm{tsupport}\left(f\right)\subseteq \mathrm{Ioo}\left(-L_1,L_1\right)\Rightarrow q\left(L_2,f\right)=q\left(L_1,f\right)\wedge \mathrm{BddBelow}\left(R_2\right)\wedge \mathrm{Nonempty}\left(R_1\right)\Rightarrow \mathrm{sInf}\left(R_2\right)\le \mathrm{sInf}\left(R_1\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaPntBounds/SupportRayleighMonotonicity.support_rayleigh_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

W is the canonical carrier of even smooth compactly supported complex tests, and l2Mass is its canonical squared real-line mass. The two displayed sets are the attained quadratic-cost values on unit-mass tests in the respective open windows.

The window-invariance premise is the source clause that the explicit formula value does not change when a smaller-supported test is viewed in a larger external window. Set inclusion and the conditional-complete-lattice infimum lemma yield the result.

References

• Truth anchor: D5/S3/Weil/ZetaPntBounds/SupportRayleighMonotonicity.support_rayleigh_monotonicity
• Dependency: D5/S3/Weil/ZetaGamma/ArchimedeanJumpDecomposition