Finite Observability Energy Balance

Abstract

The finite observability Gramian telescopes, is positive semidefinite, and measures state energy loss.

Theorem 1.1 (Finite observability identity and energy balance).

$$\begin{array}{r}\forall K,V,Y:\mathrm{Type},\\ [\mathrm{RCLike}(K)]\wedge [\mathrm{NormedAddCommGroup}(V)]\wedge [\mathrm{InnerProductSpace}(K,V)]\wedge [\mathrm{CompleteSpace}(V)]\wedge \\ [\mathrm{NormedAddCommGroup}(Y)]\wedge [\mathrm{InnerProductSpace}(K,Y)]\wedge [\mathrm{CompleteSpace}(Y)]\wedge \\ \forall A:\mathrm{ContinuousLinearMap}(K,V,V),C:\mathrm{ContinuousLinearMap}(K,V,Y),N:\mathbb{N},(\mathrm{adjoint}(A)\circ A)+(\mathrm{adjoint}(C)\circ C)=\mathrm{id}()\Rightarrow \\ \\ \mathrm{id}()-(\mathrm{adjoint}(A^N)\circ A^N)=\sum _{k\in \mathrm{range}(N)}(\mathrm{adjoint}(A^k)\circ (\mathrm{adjoint}(C)\circ C)\circ A^k)\wedge \mathrm{IsPositive}(\sum _{k\in \mathrm{range}(N)}(\mathrm{adjoint}(A^k)\circ (\mathrm{adjoint}(C)\circ C)\circ A^k))\wedge \forall x:V,{\Vert x\Vert }^2-{\Vert (A^{N}x)\Vert }^2=\sum _{k\in \mathrm{range}(N)}{\Vert (C{A}^{k}x)\Vert }^2.\end{array}$$

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

Source. Repository-derived.

Commentary.

The bounded update A and readout C act on complete inner-product spaces over a real or complex scalar field. The conservation law A* A + C* C = I is the source premise.

The finite Gramian is the explicit sum of the adjoint readout terms for k below N. The first public clause telescopes this sum against the N-step state operator.

The second clause states operator positivity, including symmetry and nonnegativity of every quadratic form. The third clause gives the corresponding finite state norm-energy balance.

Repository and pinned-library searches found no packaged theorem with all three clauses. The proof applies the adjoint-power law, finite sum telescoping, and adjoint inner-product identities directly.

References

• Truth anchor: D5/S3/Observer/Linear/FiniteObservabilityEnergyBalance.finite_observability_energy_balance