Monotonicity of the discrete-time Riccati operator on the positive semidefinite cone

Proved

BertsekasDP.riccati_map_monotone

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

control-theorylinear-quadratic-regulatormatrix-analysisriccati-equation

Let $A$ be $n \times n$ , $B$ be $n \times m$ , $Q$ be $n \times n$ , and let $R \succ 0$ be $m \times m$ . Write

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

for the discrete-time Riccati operator. If $P$ and $P'$ are positive semidefinite and $P \preceq P'$ in the Loewner order, then

F(P) \preceq F(P').

The operator therefore preserves the order of the positive semidefinite cone. This is the workhorse behind every convergence argument for the Riccati recursion: it makes the iterates started from $0$ nondecreasing, it bounds them above by any fixed point, and it lets one sandwich an arbitrary starting point between two controlled sequences.

The reason it holds is that $F(P)$ is the minimum over feedback gains $L$ of $(A+BL)^{\top}P(A+BL) + Q + L^{\top}RL$ , an expression that is itself monotone in $P$ by congruence, and a minimum of monotone functions is monotone.

Formalization Note Mathlib carries no Loewner order on matrices, so $P \preceq P'$ is stated as (P' - P).PosSemidef, and likewise for the conclusion. Positive semidefiniteness in Mathlib includes symmetry. The matrix inverse is Mathlib's total inverse; under $R \succ 0$ and $P \succeq 0$ the matrix $B^{\top}PB + R$ is positive definite, hence genuinely invertible, so the formula is the intended one.

Preamble

import Mathlib
import Definitions.Def_BertsekasRiccatiMap

open Matrix

Formal statement

namespace BertsekasDP

theorem riccati_map_monotone {n m : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (B : Matrix (Fin n) (Fin m) ℝ)
    (Q : Matrix (Fin n) (Fin n) ℝ) (R : Matrix (Fin m) (Fin m) ℝ)
    (P P' : Matrix (Fin n) (Fin n) ℝ)
    (hP : P.PosSemidef) (hP' : P'.PosSemidef) (hR : R.PosDef)
    (hle : (P' - P).PosSemidef) :
    (BertsekasRiccatiMap A B Q R P' - BertsekasRiccatiMap A B Q R P).PosSemidef := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 4.4; monotonicity of the Riccati operator on the positive semidefinite cone, used throughout the proof of Proposition 4.4.1.

View graph