Rational-Toeplitz Collapse

Abstract

A common denominator converts a rational feature Gram matrix into a congruence of one weighted monomial moment matrix.

Theorem 1.1 (A common denominator gives one moment congruence).

$$\begin{array}{r}\forall n:\mathbb{N},mu:\mathrm{FiniteMeasure}(Circle),\\ A:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),D:\mathrm{Polynomial}(\mathbb{C}),\\ hD:\forall z\in Circle,\mathrm{eval}(D,z)\ne 0,\\ \mathrm{let}(v:Circle\to \left(\mathrm{Fin}(n)\to \mathbb{C}\right),\forall z:Circle,j:\mathrm{Fin}(n),v(z)(j)=z^j\psi :Circle\to \left(\mathrm{Fin}(n)\to \mathbb{C}\right),\forall z:Circle,i:\mathrm{Fin}(n),\psi (z)(i)=\frac{\mathrm{mulVec}(A,v(z))(i)}{\mathrm{eval}(D,z)}\Sigma :\mathrm{Measure}(Circle)=\mathrm{withDensity}(mu,(z:Circle\mapsto \mathrm{ofReal}(\mathrm{normSq}(\mathrm{eval}(D,z){)}^{-1})))G:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),\forall i:\mathrm{Fin}(n),j:\mathrm{Fin}(n),G_{i,j}=\mathrm{integral}(mu,(z:Circle\mapsto \psi (z)(i)\cdot {\psi (z)(j)}^{\ast }))T:\mathrm{Matrix}(\mathrm{Fin}(n),\mathrm{Fin}(n),\mathbb{C}),\forall i:\mathrm{Fin}(n),j:\mathrm{Fin}(n),T_{i,j}=\mathrm{integral}(\Sigma ,(z:Circle\mapsto v(z)(i)\cdot {v(z)(j)}^{\ast }))),\\ G=A\cdot T\cdot \mathrm{conjTranspose}(A).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/BlockStructure/RationalToeplitzCollapse.rational_toeplitz_collapse (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite positive measure on the unit circle, a complex coefficient matrix, and a polynomial without unit-circle zeros construct the monomial and rational feature vectors.

The weighted measure uses the reciprocal norm-square of the supplied denominator. Compactness of the circle and nonvanishing of the denominator make this measure finite.

Expanding both finite matrix products and moving their scalar coefficients through the integral identifies the rational Gram matrix with the displayed congruence.

References

• Truth anchor: D5/S3/Observer/BlockStructure/RationalToeplitzCollapse.rational_toeplitz_collapse