Closed-loop stability of a positive definite Riccati fixed point (Prop. 4.4.1, part 4, conditional form)

Proved

BertsekasDP.riccati_psd_fixed_point_closed_loop_stable

by jackjburleson · 1 vote · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

control-theorylinear-quadratic-regulatorlyapunov-stabilityriccati-equation

Let $A \in \mathbb{R}^{n\times n}$ , $B \in \mathbb{R}^{n\times m}$ , $Q = C^{\top}C \succeq 0$ , $R \succ 0$ , with $(A,B)$ controllable and $(A,C)$ observable (Definition 4.1.1 of Bertsekas). Let $P \succ 0$ be a fixed point of the Riccati operator $F(P) = A^{\top}(P - PB(B^{\top}PB + R)^{-1}B^{\top}P)A + Q$ . Then the closed-loop matrix

A + BL, \qquad L = -\bigl(B^{\top}PB + R\bigr)^{-1}B^{\top}PA,

has all eigenvalues (of the complexified matrix) strictly inside the unit disk: $|\lambda| < 1$ .

Proof sketch: the Lyapunov identity obtained by expanding $F(P) = P$ around the stationary gain gives, for the closed-loop dynamics $x_{k+1} = (A + BL)x_k$ , the strict decrease

x^{\top}Px - x_{+}^{\top}Px_{+} = x^{\top}Qx + (u)^{\top}Ru \;\ge\; \|Cx\|^2 ,

where $u = Lx$ and strictness uses $R \succ 0$ . Telescoping along trajectories shows $\sum_k \|Cx_k\|^2 \le x^{\top}Px < \infty$ ; if some $\lambda$ with $|\lambda| \ge 1$ existed, an eigenvector-type trajectory would keep $\|Cx_k\|$ from being summable unless $C A^{j} v = 0$ for all $j$ , and observability (plus controllability, to handle modes reachable only through $B$ ) forces $v = 0$ — a contradiction. Hence $|\lambda| < 1$ for every closed-loop eigenvalue. This is part 4 of Bertsekas, Vol. I, Proposition 4.4.1.

Preamble

import Mathlib
import Definitions.Def_BertsekasRiccatiMap

open Matrix

Formal statement

namespace BertsekasDP

theorem riccati_psd_fixed_point_closed_loop_stable {n m q : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (B : Matrix (Fin n) (Fin m) ℝ)
    (Q : Matrix (Fin n) (Fin n) ℝ) (R : Matrix (Fin m) (Fin m) ℝ)
    (C : Matrix (Fin q) (Fin n) ℝ)
    (hQ : Q = Cᵀ * C) (hQpsd : Q.PosSemidef) (hR : R.PosDef)
    (hctrb : BertsekasControllablePair A B)
    (hobs : BertsekasObservablePair A C)
    (P : Matrix (Fin n) (Fin n) ℝ) (hP : P.PosDef)
    (hfix : BertsekasRiccatiMap A B Q R P = P) :
    ∀ z ∈ spectrum ℂ
          ((A + B * (-((Bᵀ * P * B + R)⁻¹ * Bᵀ * P * A))).map
            (algebraMap ℝ ℂ)),
        ‖z‖ < 1 := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, Athena Scientific, 3rd ed., 2005, Section 4.4, Proposition 4.4.1 (part 4); J. C. Willems, Least squares stationary optimal control and the algebraic Riccati equation, IEEE Trans. Automat. Control 16 (1971), no. 6, 621–634.

View graph