Hankel Gramian Singular Values

Abstract

The positive Hankel singular values are the square roots of the controllability-observability Gramian-product spectrum.

Theorem 1.1 (Hankel and Gramian-product spectra agree).

$$\begin{array}{c}\forall K,V,Y:Type,S,O,n,\\ \mathrm{RCLike}(K)\wedge \mathrm{NormedAddCommGroup}(V)\wedge \mathrm{InnerProductSpace}(K,V)\wedge \mathrm{FiniteDimensional}(K,V),\\ \mathrm{NormedAddCommGroup}(Y)\wedge \mathrm{InnerProductSpace}(K,Y)\wedge \mathrm{FiniteDimensional}(K,Y)\wedge S\in \mathrm{LinearMap}(K,V,V)\wedge O\in \mathrm{LinearMap}(K,V,Y),\\ \mathrm{adjoint}(S)=S\wedge \mathrm{Injective}(S)\wedge \mathrm{Injective}(O)\wedge n\in N\wedge \mathrm{finrank}(K,V)=n\Rightarrow \\ \mathrm{let}(H,\mathrm{comp}(O,S)),\mathrm{let}(P,\mathrm{comp}(S,\mathrm{comp}(\mathrm{comp}(\mathrm{adjoint}(O),O),S))),\\ \exists hP:\mathrm{IsSymmetric}(P),\forall i\in \mathrm{Fin}(n),0<\mathrm{singularValue}(H,i)\wedge \mathrm{singularValue}(H,i)=\mathrm{sqrt}(\mathrm{eigenvalue}(hP,n,i)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/HankelGramianSingularValues.hankel_gramian_singular_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Hankel map is constructed by composing the controllability root with future output. Self-adjointness identifies its adjoint-square with the displayed Gramian product; injectivity makes every indexed singular value positive.

References

• Truth anchor: D5/S3/Observer/LinearMemory/HankelGramianSingularValues.hankel_gramian_singular_values