Riccati convergence and closed-loop stability (Prop. 4.4.1)

Proved

BertsekasDP.riccati_convergence_stability

by Shuze Chen · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

lqrriccatiequationstability

Proposition 4.4.1 (asymptotic behavior of the Riccati equation and closed-loop stability). Let $A$ be $n \times n$ , $B$ be $n \times m$ , let $Q$ be positive semidefinite symmetric with $Q = C^{\top} C$ , and let $R$ be positive definite symmetric. Assume that $(A,B)$ is controllable and that $(A,C)$ is observable. Then there is a positive definite symmetric matrix $P$ such that:

$P$ solves the algebraic Riccati equation:

P \;=\; A^{\top}\Bigl(P - P B \bigl(B^{\top} P B + R\bigr)^{-1} B^{\top} P\Bigr) A + Q ;

$P$ is the only positive semidefinite solution: every positive semidefinite fixed point of the Riccati operator equals $P$ ;
the Riccati iteration converges to $P$ from every positive semidefinite start:

\lim_{k \to \infty} P_k \;=\; P \qquad \text{whenever } P_{k+1} = F(P_k), \; P_0 \succeq 0 ;

the closed loop is stable: with the stationary gain $L = -\bigl(B^{\top} P B + R\bigr)^{-1} B^{\top} P A$ , every eigenvalue $\lambda$ of $A + BL$ satisfies

|\lambda| \;<\; 1 .

This is the mathematical warrant for steady-state LQR design: it says the design equation has exactly one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting constant feedback law stabilizes the system. Without part 4 one could compute a gain that minimizes cost over a finite horizon yet drives the state to infinity as the horizon grows.

Formalization Note Positive semidefiniteness and definiteness are Mathlib's (symmetry included). Uniqueness is asserted within the positive semidefinite cone only; nothing is claimed about indefinite fixed points. Convergence is entrywise, equivalently in any matrix norm. Eigenvalues are taken as the spectrum of the complexified matrix, so the bound is on the complex modulus. Matrix inverses are Mathlib's total inverse; part of the proof burden is showing $B^{\top}PB + R$ is invertible where it is used.

Preamble

import Mathlib
import Definitions.Def_BertsekasRiccatiMap

open Matrix

Formal statement

namespace BertsekasDP

theorem riccati_convergence_stability {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) ℝ, P.PosDef ∧
      BertsekasRiccatiMap A B Q R P = P ∧
      (∀ P' : Matrix (Fin n) (Fin n) ℝ, P'.PosSemidef →
        BertsekasRiccatiMap A B Q R P' = P' → P' = P) ∧
      (∀ P₀ : Matrix (Fin n) (Fin n) ℝ, P₀.PosSemidef →
        Filter.Tendsto (fun k => (BertsekasRiccatiMap A B Q R)^[k] P₀)
          Filter.atTop (nhds 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, 3rd ed., Athena Scientific, 2005, Proposition 4.4.1 (Section 4.1)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $n, m, q$ be natural numbers (implicit arguments; each may be $0$ ), and let $A$ ( $n \times n$ ), $B$ ( $n \times m$ ), $Q$ ( $n \times n$ ), $R$ ( $m \times m$ ), $C$ ( $q \times n$ ) be real matrices. Write $F$ for the bundle's Riccati map with data $(A, B, Q, R)$ :

F(P) \;=\; A^{\mathsf T}\Bigl(P - P B\,\bigl(B^{\mathsf T} P B + R\bigr)^{-1} B^{\mathsf T} P\Bigr) A + Q,

where $(\cdot)^{-1}$ is the total matrix inverse that returns the zero matrix on singular input (so for a given argument $P$ the middle term silently vanishes if $B^{\mathsf T} P B + R$ happens to be singular). The hypotheses are:

$Q = C^{\mathsf T} C$ ;
$Q$ is positive semidefinite (symmetric, and $x^{\mathsf T} Q x \ge 0$ for all $x \in \mathbb{R}^n$ ) — a hypothesis stated separately even though it already follows from $Q = C^{\mathsf T} C$ ;
$R$ is positive definite (symmetric, and $x^{\mathsf T} R x > 0$ for all $x \ne 0$ ; for $m = 0$ this holds vacuously);
the pair $(A, B)$ satisfies the bundle's controllability property: the $n \times (n\cdot m)$ matrix with blocks $A^i B$ , $i = 0, \dots, n-1$ , has rank $n$ over $\mathbb{R}$ ;
the pair $(A, C)$ satisfies the bundle's observability property, i.e. the transposed pair $(A^{\mathsf T}, C^{\mathsf T})$ satisfies the controllability property: the $n \times (n \cdot q)$ matrix with blocks $(A^{\mathsf T})^i C^{\mathsf T}$ , $i = 0, \dots, n-1$ , has rank $n$ .

The conclusion asserts the existence of a real $n \times n$ matrix $P$ satisfying the conjunction of five claims:

$P$ is positive definite (symmetric, and $x^{\mathsf T} P x > 0$ for all $x \ne 0$ );
$P$ is a fixed point of the Riccati map: $F(P) = P$ ;
$P$ is the unique positive-semidefinite fixed point: every real $n\times n$ matrix $P'$ that is positive semidefinite and satisfies $F(P') = P'$ equals $P$ (nothing is claimed about fixed points that are not positive semidefinite);
for every positive-semidefinite $n \times n$ matrix $P_0$ , the iterates $F^{[k]}(P_0)$ (the $k$ -fold application of $F$ , with $F^{[0]}(P_0) = P_0$ ) converge to $P$ as $k \to \infty$ , in the standard (entrywise) topology on real matrices;
writing $L = -\bigl(B^{\mathsf T} P B + R\bigr)^{-1} B^{\mathsf T} P A$ (an $m \times n$ matrix, again using the total inverse with zero-matrix junk value on singular input), every element $z$ of the spectrum over $\mathbb{C}$ of the complexification of the closed-loop matrix $A + B L$ — i.e. of the complex $n \times n$ matrix obtained by mapping each real entry of $A + BL$ into $\mathbb{C}$ ; for a matrix over the field $\mathbb{C}$ this spectrum is exactly the set of complex eigenvalues — satisfies the strict bound $\lVert z \rVert < 1$ (complex modulus).

Edge cases the statement silently includes: if $n = 0$ , both rank hypotheses hold trivially, all matrix conditions are vacuous, and the spectrum in clause 5 is empty; if $n > 0$ and $m = 0$ (or $q = 0$ ), the controllability (resp. observability) hypothesis is false, making the theorem vacuous for those dimensions.

Human review

Endorsed by Community (Bot) · Sep 8, 2026
Endorsed by Shuze Chen · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph