Target Observability Four-Way Equivalence

Abstract

A linear target is observable exactly when its Riesz vector lies in the adjoint range.

Theorem 1.1 (Four equivalent criteria for linear target observability).

$$\begin{array}{c}\forall K,X,Y:Type,\\ \mathrm{RCLike}(K)\wedge \mathrm{NormedAddCommGroup}(X)\wedge \mathrm{InnerProductSpace}(K,X)\wedge \mathrm{FiniteDimensional}(K,X)\wedge \\ \mathrm{NormedAddCommGroup}(Y)\wedge \mathrm{InnerProductSpace}(K,Y)\wedge \mathrm{FiniteDimensional}(K,Y)\Rightarrow \\ \forall M:\mathrm{LinearMap}(K,X,Y),t:\mathrm{LinearMap}(K,X,K),v_t:X,\\ (\forall x:X,t(x)=\mathrm{inner}(v_t,x))\Rightarrow \\ ((\forall x,y:X,M(x)=M(y)\Rightarrow t(x)=t(y))⟺\ker (M)\subseteq \ker (t))\wedge \\ ((\forall x,y:X,M(x)=M(y)\Rightarrow t(x)=t(y))⟺v_t\in \mathrm{range}(\mathrm{adjoint}(M)))\wedge \\ ((\forall x,y:X,M(x)=M(y)\Rightarrow t(x)=t(y))⟺\exists a:Y,\mathrm{adjoint}(M)(a)=v_t)\wedge \\ (\forall a:Y,\mathrm{adjoint}(M)(a)=v_t\Rightarrow \forall x:X,t(x)=\mathrm{inner}(a,M(x))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/VisibleDescent/TargetObservabilityFourWayEquivalence.target_observability_four_way_equivalence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target functional is represented on the source Hilbert space by its displayed Riesz vector. Constancy on observation fibers is equivalent to inclusion of the observation kernel in the target kernel.

Finite-dimensional orthogonal duality identifies that condition with membership of the Riesz vector in the adjoint range. Every displayed adjoint preimage reconstructs the target from the observation.

References

• Truth anchor: D5/S3/Observer/VisibleDescent/TargetObservabilityFourWayEquivalence.target_observability_four_way_equivalence