Exact Truncated Haar Floor

Abstract

A represented Hermitian truncated circle moment vector has exact normalized-Haar floor equal to its least Toeplitz eigenvalue.

Theorem 1.1 (Exact truncated Haar floor).

$$\forall N\in \mathbb{N},m\in \mathbb{Z}\to \mathbb{C},R\in \mathbb{R},\left(\left(\left(\left(\left(\left(\left(\left(\forall ell\in \mathbb{Z},m\left(\mathrm{neg}\left(ell\right)\right)=\mathrm{star}\left(m\left(ell\right)\right)\right)\wedge m\left(0\right)=\mathrm{toComplex}\left(R\right)\right)\wedge 0<R\right)\wedge \left(\exists mu\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),\forall ell\in \mathbb{Z},\mathrm{natAbs}\left(ell\right)\le N\Rightarrow \mathrm{integral}\left(z,\mathrm{Circle}\left(\right),\mathrm{zpow}\left(z,\mathrm{neg}\left(ell\right)\right),mu\right)=m\left(ell\right)\right)\right)\wedge \mathrm{let}T=\mathrm{Matrix}\left((j,k\in \mathrm{Fin}\left(N+1\right)\mapsto m\left(\mathrm{toInt}\left(j\right)-\mathrm{toInt}\left(k\right)\right))\right)\right)\wedge \mathrm{let}hT=\mathrm{hermitianToeplitz}\left(m,\forall ell\in \mathbb{Z},m\left(\mathrm{neg}\left(ell\right)\right)=\mathrm{star}\left(m\left(ell\right)\right)\right):\mathrm{IsHermitian}\left(T\right)\right)\wedge \mathrm{let}A=\left\{\exists mu\in \mathrm{FiniteMeasure}\left(\mathrm{Circle}\left(\right)\right),\left(\forall ell\in \mathbb{Z},\mathrm{natAbs}\left(ell\right)\le N\Rightarrow \mathrm{integral}\left(z,\mathrm{Circle}\left(\right),\mathrm{zpow}\left(z,\mathrm{neg}\left(ell\right)\right),mu\right)=m\left(ell\right)\right)\wedge \mathrm{toMeasure}\left(\mathrm{smul}\left(alpha,\mathrm{normalizedCircleHaar}\left(\right)\right)\right)\le \mathrm{toMeasure}\left(mu\right)\mid alpha\in \mathrm{NonnegativeReal}\left(\right)\right\}\right)\wedge \mathrm{let}alphaN=\mathrm{sSup}\left(A\right)\right)\Rightarrow \mathrm{toReal}\left(alphaN\right)=\mathrm{lambdaMin}\left(T,hT\right)$$

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

Source. Repository-derived.

Commentary.

The Toeplitz matrix and feasible floor set are constructed directly from the supplied truncated moment data and normalized circle Haar measure.

The forward bound subtracts any dominated Haar component and uses positivity of the residual Toeplitz matrix. For the reverse bound, a local finite trigonometric-moment proof constructs a positive atomic circle measure from the positive semidefinite shifted Toeplitz matrix.

The positive zeroth moment bounds the feasible floors, so their supremum is well-defined and equals the least ordered Hermitian eigenvalue.

References

• Truth anchor: D5/S3/Weil/TestFunctions/ExactTruncatedHaarFloor.exact_truncated_haar_floor
• Dependency: D5/S3/Weil/CayleyLaguerre/TruncatedCircleMomentBridge
• Dependency: D5/S3/Weil/TestFunctions/ToeplitzContactSupport