Observability Gramian Kernel and Energy

Abstract

The stable ordinary observability Gramian has the all-future readout kernel, its quadratic form is total future output energy, and that energy vanishes exactly on states with no future output.

Theorem 1.1 (The ordinary Gramian kernel is the all-future kernel).

$$\begin{array}{r}\forall K,V,Y:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{NormedAddCommGroup}(V)],\\ [\mathrm{InnerProductSpace}(K,V)],[\mathrm{FiniteDimensional}(K,V)],\\ [\mathrm{NormedAddCommGroup}(Y)],[\mathrm{InnerProductSpace}(K,Y)],\\ [\mathrm{FiniteDimensional}(K,Y)],\\ \forall T:\mathrm{LinearMap}(K,V,V),C:\mathrm{LinearMap}(K,V,Y),\\ hStable:\mathrm{Summable}(k\mapsto \mathrm{discountedGramianTerm}(T,C,1,k)),\\ \ker (\mathrm{toLinearMap}(\mathrm{discountedObservabilityGramian}(T,C,1)))={\mathrm{intersection}}_{k\in \mathbb{N}}\ker (\mathrm{comp}(C,T^k))\wedge \\ (\forall x:V,\Re (⟨x,\mathrm{discountedObservabilityGramian}(T,C,1)(x)⟩)=\sum _{k=0}^{\infty }{\Vert C(T^k(x))\Vert }^2)\wedge \\ (\forall x:V,\Re (⟨x,\mathrm{discountedObservabilityGramian}(T,C,1)(x)⟩)=0⟺\forall k:\mathbb{N},C(T^k(x))=0).\end{array}$$

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

Source. Repository-derived.

Commentary.

The ordinary Gramian is the canonical weight-one instance of the repository’s Gramian series. Stability is stated directly as summability of that exact operator series, without imposing a stronger contraction-norm condition.

Continuous evaluation, inner product, and real-part maps carry the summable operator series term by term. Each term is the squared norm of one future readout, so nonnegativity makes zero total energy equivalent to vanishing at every future time.

References

• Truth anchor: D5/S3/Observer/LinearMemory/ObservabilityGramianKernelEnergy.observability_gramian_kernel_energy
• Dependency: D5/S3/Observer/Linear/DiscountedObservabilityGramianPositivity
• Dependency: D5/S3/ObserverMemory/Dynamics/MaximalUnobservableSubspace