Observation Rank Equality

Abstract

A finite-dimensional readout and its two Gram compositions have the same rank.

Theorem 1.1 (Readout, state Gramian, and observable Gramian have equal rank).

$$\begin{array}{c}\forall K,X,P:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{NormedAddCommGroup}(X)],[\mathrm{InnerProductSpace}(K,X)],[\mathrm{NormedAddCommGroup}(P)],[\mathrm{InnerProductSpace}(K,P)],\\ [\mathrm{FiniteDimensional}(K,X)],[\mathrm{FiniteDimensional}(K,P)],\\ M:\mathrm{LinearMap}(K,X,P)\Rightarrow \\ finrank(K)\mathrm{range}(\mathrm{adjointComp}(M))=finrank(K)\mathrm{range}(M)\wedge finrank(K)\mathrm{range}(M)=finrank(K)\mathrm{range}(\mathrm{compAdjoint}(M)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The source readout map is a linear map between finite-dimensional inner-product spaces. Its adjoint composition on the state space and the reverse composition on the readout space have ranges of the same finite rank as the readout itself.

References

• Truth anchor: D5/S3/Observer/LinearMemory/ObservationRankEquality.observation_rank_equality