The Riccati operator as a minimum over feedback gains: completion of the square

Proved

BertsekasDP.riccati_completion_of_square

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$ , let $Q$ be $n \times n$ , and let $P$ and $R$ be symmetric with $D = B^{\top}PB + R$ invertible. For a feedback gain $L$ write

G(P,L) = (A+BL)^{\top} P (A+BL) + Q + L^{\top} R L

for the one-stage cost matrix under the stationary law $u = Lx$ , and let $F$ denote the discrete-time Riccati operator. Setting

L^{*}(P) = -D^{-1}B^{\top}PA ,

the two are related by an exact completion of the square:

G(P,L) = F(P) + \bigl(L - L^{*}(P)\bigr)^{\top} D \bigl(L - L^{*}(P)\bigr) .

When $D \succ 0$ the correction term is positive semidefinite and vanishes exactly at $L = L^{*}(P)$ , so the identity says that $F(P) = \min_{L} G(P,L)$ , the minimum being attained at $L^{*}(P)$ . This is the algebraic content of the Riccati recursion: the opaque expression $-PB(B^{\top}PB+R)^{-1}B^{\top}P$ is precisely what optimizing the feedback at one stage produces.

The identity is the natural entry point for the asymptotic theory. Monotonicity of $F$ , invariance of the positive semidefinite cone, and the one-step dynamic programming inequality all follow from it directly. It holds as a pure algebraic identity, with no positivity assumption beyond invertibility of $D$ .

Formalization Note The difference $L - L^{*}(P)$ is written out as $L + D^{-1}B^{\top}PA$ , so that no definition of the optimal gain is needed. Symmetry of $P$ and $R$ is used to collect the cross terms via $A^{\top}PB = (B^{\top}PA)^{\top}$ and $(D^{-1})^{\top} = D^{-1}$ . The hypothesis is invertibility of the determinant, which is what Mathlib's total inverse requires in order to satisfy $D D^{-1} = 1$ .

Preamble

import Mathlib
import Definitions.Def_BertsekasRiccatiMap

open Matrix

Formal statement

namespace BertsekasDP

theorem riccati_completion_of_square {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 : Matrix (Fin n) (Fin n) ℝ) (L : Matrix (Fin m) (Fin n) ℝ)
    (hP : Pᵀ = P) (hR : Rᵀ = R) (hD : IsUnit (Bᵀ * P * B + R).det) :
    (A + B * L)ᵀ * P * (A + B * L) + Q + Lᵀ * R * L
      = BertsekasRiccatiMap A B Q R P
        + (L + (Bᵀ * P * B + R)⁻¹ * (Bᵀ * P * A))ᵀ * (Bᵀ * P * B + R)
          * (L + (Bᵀ * P * B + R)⁻¹ * (Bᵀ * P * A)) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 4.1, Eq. (4.8) and the accompanying completion-of-the-square derivation of the optimal stationary gain.

View graph