White Floor and Sampling Duality

Abstract

A spectral quadratic identity identifies the local white floor with the least unit-norm sampling energy.

Theorem 1.1 (White floor equals the least sampling bound).

$$\forall H\in Type,K\in Type,quadratic\in H\to \mathrm{Real}\left(\right),sampling\in \mathrm{ContinuousLinearMap}\left(\mathrm{Real}\left(\right),H,K\right),\left(\mathrm{NormedAddCommGroup}\left(H\right)\wedge \left(\mathrm{NormedSpace}\left(\mathrm{Real}\left(\right),H\right)\wedge \left(\mathrm{Nontrivial}\left(H\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(K\right)\wedge \left(\mathrm{NormedSpace}\left(\mathrm{Real}\left(\right),K\right)\wedge \left(\forall f\in H,\mathrm{apply}\left(quadratic,f\right)={\Vert \mathrm{apply}\left(sampling,f\right)\Vert }^2\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}whiteFloors=\left\{\forall f\in H,0\le \mathrm{sub}\left(\mathrm{apply}\left(quadratic,f\right),\mathrm{mul}\left(lambda,{\Vert f\Vert }^2\right)\right)\mid lambda\in \mathrm{Real}\left(\right)\right\},\mathrm{let}samplingBounds=\left\{\exists f\in H,\Vert f\Vert =1\wedge r={\Vert \mathrm{apply}\left(sampling,f\right)\Vert }^2\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{sSup}\left(whiteFloors\right)=\mathrm{sInf}\left(samplingBounds\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/WhiteFloorSamplingDuality.white_floor_sampling_frame_duality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cone-margin theorem first expresses the floor as a nonzero Rayleigh infimum. Normalizing each nonzero test vector proves that this value set is exactly the unit-sphere sampling set.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/WhiteFloorSamplingDuality.white_floor_sampling_frame_duality
• Dependency: D5/S3/Weil/ZetaAnalytic/LocalSpectralFloor