Observability makes the unobservable subspace trivial

Proved

BertsekasDP.observable_pair_left_kernel_trivial

by olivier · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

control-theorylinear-algebramatrix-analysisobservability

Let $A$ be $n \times n$ and $C$ be $q \times n$ , and suppose the pair $(A,C)$ is observable in the sense of Definition 4.1.1 of Bertsekas, that is, the pair $(A^{\top}, C^{\top})$ is controllable. If a vector $x \in \mathbb{R}^{n}$ satisfies

C A^{j} x = 0 \qquad \text{for every } j \ge 0 ,

then $x = 0$ .

In words: a state producing the identically zero output under the free dynamics must itself be zero. This is the operational meaning of observability, and it is the form in which the hypothesis is actually consumed in proofs, as opposed to the rank condition in which it is usually stated.

The passage from one to the other is short. Observability makes the observability matrix surjective, so a vector annihilating all of its columns is orthogonal to the whole space, in particular to itself.

Formalization Note The hypothesis is stated for every natural $j$ rather than for $j < n$ . This is the convenient form at the point of use, and it is the weaker of the two hypotheses, since the finite family already determines the infinite one through the Cayley-Hamilton theorem. Observability is the platform definition BertsekasObservablePair, itself the controllability of the transposed pair, expressed as a rank condition.

Preamble

import Mathlib
import Definitions.Def_BertsekasRiccatiMap

open Matrix

Formal statement

namespace BertsekasDP

theorem observable_pair_left_kernel_trivial {n q : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (C : Matrix (Fin q) (Fin n) ℝ)
    (hobs : BertsekasObservablePair A C) (x : Fin n → ℝ)
    (hx : ∀ j : ℕ, C *ᵥ ((A ^ j) *ᵥ x) = 0) : x = 0 := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 4.1, Definition 4.1.1 (observability), together with the standard equivalence with triviality of the unobservable subspace.

View graph