Optimality condition (Prop. 7.2.1(d))

Proved

BertsekasDP.ssp_optimality_condition

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

optimalitycondition

Proposition 7.2.1(d) (optimality condition). Under Assumption 7.2.1, let $J^*$ solve Bellman's equation and let $\mu$ be an admissible stationary policy with evaluated cost $J_\mu$ . Then $\mu$ is optimal if and only if it attains the minimum in Bellman's equation at every state:

J_\mu = J^* \qquad \Longleftrightarrow \qquad g\bigl(i, \mu(i)\bigr) + \sum_{j=1}^{n} p_{ij}\bigl(\mu(i)\bigr) J^*(j) \;=\; \min_{u \in U(i)} \Bigl[\, g(i,u) + \sum_{j=1}^{n} p_{ij}(u) J^*(j) \,\Bigr] \quad \text{for all } i .

In words: the optimal policies are exactly the policies that are greedy with respect to the optimal cost vector. This is what turns the solution of Bellman's equation into a controller — one reads off an optimal policy by minimizing state by state — and it is the criterion by which policy iteration recognizes that it has finished.

Formalization Note $J^*$ and $J_\mu$ enter as given fixed points of $T$ and $T_\mu$ respectively; their uniqueness is not assumed here, being supplied by Prop. 7.2.1(b),(c). Both directions of the equivalence are asserted.

Preamble

import Mathlib
import Definitions.Def_BertsekasSSPModel

Formal statement

namespace BertsekasDP

theorem ssp_optimality_condition {n : ℕ} {C : Type} [Fintype C]
    (M : BertsekasSSPModel n C)
    (hA : ∃ m : ℕ, 0 < m ∧ ∀ π, BertsekasSSPAdmissible M π →
      ∀ i, BertsekasSSPSurvival M π m i < 1)
    (Jstar : Fin n → ℝ) (hbell : BertsekasSSPBellmanOp M Jstar = Jstar)
    (μ : Fin n → C) (hμ : ∀ i, μ i ∈ M.U i)
    (Jμ : Fin n → ℝ) (heval : BertsekasSSPPolicyOp M μ Jμ = Jμ) :
    Jμ = Jstar ↔
      ∀ i, M.g i (μ i) + ∑ j, M.p i (μ i) j * Jstar j =
        BertsekasSSPBellmanOp M Jstar i := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 7.2.1(d)

Read-back

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

Let $M$ be a BertsekasSSPModel on $n$ states with finite control type $C$ . Assume:

$hA$ : there is an $m > 0$ such that for every admissible policy sequence $\pi$ and every state $i$ , $S^m_\pi(i) < 1$ (the $m$ -step survival mass, as defined in this bundle);
$J^* : \{0,\dots,n-1\} \to \mathbb{R}$ is a function given as a hypothesis together with the assumption $T J^* = J^*$ , where $T$ is the SSP Bellman operator (no uniqueness or optimality of $J^*$ is assumed — only that it is some fixed point of $T$ );
$\mu : \{0,\dots,n-1\} \to C$ is a stage policy with $\mu(i) \in U(i)$ for every $i$ ;
$J_\mu : \{0,\dots,n-1\} \to \mathbb{R}$ is a function given with the assumption $T_\mu J_\mu = J_\mu$ (again only some fixed point of the policy operator; uniqueness is not assumed).

The conclusion is a genuine if and only if:

J_\mu = J^* \iff \forall i,\quad g(i,\mu(i)) + \sum_{j} p_{ij}(\mu(i))\, J^*(j) = (T J^*)(i),

i.e. $J_\mu$ equals $J^*$ (as functions) exactly when, at every state $i$ , the control $\mu(i)$ attains the minimum in the Bellman operator applied to $J^*$ (the left side of the displayed equality is the $\mu$ -value at $i$ , the right side is the minimum over $u \in U(i)$ ). Both directions of the equivalence are asserted. The proof is a placeholder.

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