Discounted Observability Gramian Positivity

Abstract

A convergent discounted observability Gramian is positive semidefinite.

Theorem 1.1 (The discounted observability Gramian is positive semidefinite).

$$\begin{gathered} \forall K,V,Y,T,C,\beta , \\ \mathrm{RCLike}(K)\wedge \mathrm{FiniteDimensional}(K,V)\wedge \mathrm{FiniteDimensional}(K,Y)\wedge \\ 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 0\le W_{\beta }. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/DiscountedObservabilityGramianPositivity.discounted_observability_gramian_nonnegative (✓ 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 on these source carriers.

The Gramian is constructed as the norm-convergent infinite sum of the discounted adjoint Gram terms. Its public assumptions retain both the source discount range and the stated square-root norm bound.

Each summand is a nonnegative real scalar multiple of an adjoint composition. A geometric majorant proves summability, and continuous evaluation, inner product, and real-part maps carry the operator sum to a sum of nonnegative quadratic forms.

Repository searches found no existing discounted observability Gramian theorem. The proof directly applies the pinned library’s adjoint-composition positivity, operator norm bounds, geometric summability, and infinite-sum transport lemmas.

References

• Truth anchor: D5/S3/Observer/Linear/DiscountedObservabilityGramianPositivity.discounted_observability_gramian_nonnegative