Controllability Gramian Reachable Range

Abstract

The stable ordinary controllability Gramian has exactly the reachable-state range.

Theorem 1.1 (The controllability Gramian range is reachable).

$$\begin{array}{r}\forall K,V,U:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{NormedAddCommGroup}(V)],\\ [\mathrm{InnerProductSpace}(K,V)],[\mathrm{FiniteDimensional}(K,V)],\\ [\mathrm{NormedAddCommGroup}(U)],[\mathrm{InnerProductSpace}(K,U)],\\ [\mathrm{FiniteDimensional}(K,U)],\\ \forall A:\mathrm{LinearMap}(K,V,V),B:\mathrm{LinearMap}(K,U,V),\\ \mathrm{Summable}(\mathrm{discountedGramianTerm}(\mathrm{adjoint}(A),\mathrm{adjoint}(B),1))\Rightarrow \mathrm{range}(\mathrm{toLinearMap}(\mathrm{controllabilityGramian}(A,B)))=\mathrm{reachableSubspace}(A,B).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Dynamics/ControllabilityGramianReachableRange.controllability_gramian_range_eq_reachable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The controllability Gramian is constructed as the weight-one observability Gramian of the adjoint system, so its terms are the source operators A^k B B-adjoint (A-adjoint)^k. The displayed summability premise is the exact series form of stability.

The imported ordinary-Gramian theorem identifies its kernel with the all-future adjoint-input kernel. Infinite observability duality turns that kernel into the orthogonal complement of the canonical reachable span; self-adjointness then identifies the range.

References

• Truth anchor: D5/S3/Observer/Dynamics/ControllabilityGramianReachableRange.controllability_gramian_range_eq_reachable
• Dependency: D5/S3/Observer/LinearMemory/ObservabilityGramianKernelEnergy
• Dependency: D5/S3/Observer/LinearMemory/ReachableObservableQuotientReachability
• Dependency: D5/S3/ObserverMemory/Dynamics/InfiniteObservabilityOrthogonalDuality