Hankel Rank Minimality

Abstract

Once both finite horizons reach the state-space dimension, the block Hankel rank is the reachable dimension minus the invisible reachable dimension.

Theorem 1.1 (Stable Hankel rank counts visible reachable directions).

$$\begin{array}{c}\forall K,V,U,Y:Type,\\ \mathrm{Field}(K)\wedge \mathrm{AddCommGroup}(V)\wedge \mathrm{Module}(K,V)\wedge \mathrm{FiniteDimensional}(K,V)\wedge \\ \mathrm{AddCommGroup}(U)\wedge \mathrm{Module}(K,U)\wedge \mathrm{AddCommGroup}(Y)\wedge \mathrm{Module}(K,Y)\wedge \\ A\in \mathrm{LinearMap}(K,V,V)\wedge B\in \mathrm{LinearMap}(K,U,V)\wedge C\in \mathrm{LinearMap}(K,V,Y)\wedge \\ r,s\in N,\mathrm{finrank}(K,V)\le r\wedge \mathrm{finrank}(K,V)\le s\Rightarrow \\ \mathrm{finrank}(K,\mathrm{range}(\mathrm{finiteHankel}(A,B,C,r,s)))=\mathrm{finrank}(K,\mathrm{reachableSubspace}(A,B))-\mathrm{finrank}(K,\inf (\mathrm{reachableSubspace}(A,B),\mathrm{eventualKernel}(C,A))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hankel/HankelRankMinimality.hankel_rank_eq_reachable_dim_sub_inter_unobservable_dim (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be the state evolution, B the input map, and C the readout of a finite-dimensional linear system over a field. The finite Hankel map has block (i,j) equal to C A^(i+j) B.

For row and column horizons at least finrank(K,V), its range has dimension equal to the imported reachable subspace dimension minus the dimension of its intersection with the imported all-future kernel.

References

• Truth anchor: D5/S3/Observer/Hankel/HankelRankMinimality.hankel_rank_eq_reachable_dim_sub_inter_unobservable_dim
• Dependency: D5/S3/Observer/LinearMemory/ReachableObservableQuotientReachability