LQG cost difference from the certainty-equivalent policy

Proved

BertsekasDP.lqg_cost_difference

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

control-theorydynamic-programminglinear-quadraticstochastic-control

For the finite-horizon linear-quadratic problem with imperfect state information, let $L_k$ be the gains of the underlying deterministic problem, $K_{k+1}$ the Riccati matrix, and $\hat x^{\pi}_k = \mathbb{E}[x_k \mid I_k]$ the least-squares state estimate along the closed loop generated by a policy $\pi$ .

Let $\pi^{*}$ be certainty-equivalent along its own trajectories, that is $\pi^{*}(I_k) = L_k \hat x^{\pi^{*}}_k$ at every stage $k < N$ and every outcome of positive probability.

Then for every information-feedback policy $\pi$ the cost gap is exactly a weighted sum of squared control defects:

J(\pi) - J(\pi^{*}) \;=\; \sum_{k=0}^{N-1} \mathbb{E}\Bigl[\bigl(\pi(I_k) - L_k \hat x^{\pi}_k\bigr)^{\top} \bigl(B_k^{\top} K_{k+1} B_k + R_k\bigr) \bigl(\pi(I_k) - L_k \hat x^{\pi}_k\bigr)\Bigr].

This is the completion-of-squares step behind the separation theorem: stage by stage every term that does not involve the control cancels between the two policies, and what remains measures only how far $\pi$ departs from applying the deterministic gain to the current estimate. Together with positive semidefiniteness of the stage weight it gives optimality of $\pi^{*}$ at once.

A proof should lean on the already-proved lemma BertsekasDP.lqg_estimation_error_policy_independent: the estimation error $x_k - \hat x_k$ does not depend on the policy, which is what allows the estimate to replace the true state in the completed square without disturbing the cross terms.

Preamble

import Mathlib
import Definitions.Def_BertsekasLQGModel

open Matrix

Formal statement

namespace BertsekasDP

theorem lqg_cost_difference {n m q : ℕ} {Ω₀ ΩW ΩV : Type}
    [Fintype Ω₀] [Fintype ΩW] [Fintype ΩV]
    (M : BertsekasLQGModel n m q Ω₀ ΩW ΩV)
    (πstar : List (Fin q → ℝ) → Fin m → ℝ)
    (hstar : ∀ k < M.N, ∀ ω : BertsekasLQGSample M,
      BertsekasLQGProb M ω ≠ 0 →
      πstar ((BertsekasLQGTraj M πstar k ω).2) =
        BertsekasLQGGain M k *ᵥ BertsekasLQGEstimate M πstar k ω)
    (π : List (Fin q → ℝ) → Fin m → ℝ) :
    BertsekasLQGCost M π - BertsekasLQGCost M πstar =
      ∑ k ∈ Finset.range M.N, ∑ ω : BertsekasLQGSample M,
        BertsekasLQGProb M ω *
          ((π (BertsekasLQGTraj M π k ω).2 -
              BertsekasLQGGain M k *ᵥ BertsekasLQGEstimate M π k ω) ⬝ᵥ
            (((M.B k)ᵀ * BertsekasLQGRiccati M (M.N - (k + 1)) * M.B k + M.R k) *ᵥ
              (π (BertsekasLQGTraj M π k ω).2 -
                BertsekasLQGGain M k *ᵥ BertsekasLQGEstimate M π k ω))) := by
  sorry

end BertsekasDP

Source

Dimitri P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Section 5.2 (linear systems with imperfect state information; separation theorem). The identity is the completion-of-squares step of that derivation.

View graph