Discounted Observability Gramian Kernel

Abstract

The discounted observability Gramian kernel is the all-future readout kernel.

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

$$\begin{gathered} \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)] \\ T:\mathrm{LinearMap}(K,V,V),C:\mathrm{LinearMap}(K,V,Y),\beta :\mathbb{R}, \\ {N}_{\infty }=\mathrm{iInf}(n,\ker (C\circ T^n)), \\ 0<\beta <1\wedge \sqrt{\beta }\Vert T\Vert <1\Rightarrow \\ {W}_{\beta }=\sum _{n=0}^{\infty }{\beta }^n{T^{\ast }}^n{C}^{\ast }C{T}^n\wedge \ker (W_{\beta })=N_{\infty }. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/DiscountedObservabilityGramianKernel.discounted_observability_gramian_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let V and Y be finite-dimensional inner-product spaces over a real or complex scalar field. The evolution T and readout C are arbitrary linear maps, and beta satisfies the stated discount and norm convergence restrictions.

The Gramian is the norm-convergent sum of the discounted adjoint Gram terms constructed in the positivity result. The right side is the canonical all-future readout kernel imported from the observer memory family.

Each quadratic-form summand is beta to the nth power times the squared norm of the nth observed iterate. Since every term is nonnegative and beta is positive, zero total energy is equivalent to every future readout vanishing.

Repository searches found no packaged Gramian-kernel theorem. The proof applies the pinned library’s adjoint norm identity, transport of summable series through continuous maps, and strict positivity of a nonnegative series containing a positive term.

References

• Truth anchor: D5/S3/Observer/Linear/DiscountedObservabilityGramianKernel.discounted_observability_gramian_kernel
• Dependency: D5/S3/Observer/Linear/DiscountedObservabilityGramianPositivity
• Dependency: D5/S3/ObserverMemory/Dynamics/MaximalUnobservableSubspace