Positive semidefiniteness of the LQG stage weight

Proved

BertsekasDP.lqg_stage_weight_nonneg

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

control-theorylinear-algebralinear-quadratic

In the finite-horizon linear-quadratic problem the stage weight appearing in the control-defect term is

S_k \;=\; B_k^{\top} K_{k+1} B_k + R_k,

where $K_{k+1}$ is the Riccati matrix of the underlying deterministic problem and $R_k \succ 0$ is the control cost. The claim is that $S_k$ is positive semidefinite, that is $y^{\top} S_k y \ge 0$ for every vector $y$ .

Two facts combine: $R_k$ is positive definite by assumption, and every Riccati matrix $K_j$ is positive semidefinite, being the cost-to-go matrix of a problem with $Q_j \succeq 0$ and $R_j \succ 0$ ; hence $y^{\top} B^{\top} K B y = (By)^{\top} K (By) \ge 0$ . This is what makes each term of the cost-difference decomposition a genuine penalty rather than a saving.

Preamble

import Mathlib
import Definitions.Def_BertsekasLQGModel

open Matrix

Formal statement

namespace BertsekasDP

theorem lqg_stage_weight_nonneg {n m q : ℕ} {Ω₀ ΩW ΩV : Type}
    [Fintype Ω₀] [Fintype ΩW] [Fintype ΩV]
    (M : BertsekasLQGModel n m q Ω₀ ΩW ΩV)
    (k : ℕ) (y : Fin m → ℝ) :
    0 ≤ y ⬝ᵥ (((M.B k)ᵀ * BertsekasLQGRiccati M (M.N - (k + 1)) * M.B k + M.R k) *ᵥ y) := by
  sorry

end BertsekasDP

Source

Dimitri P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Sections 4.1 and 5.2 (Riccati recursion and the gain matrices).

View graph