Theorem 1 (Robust Dynamic Programming) — perfect duality and the robust Bellman recursion

Proved

RobustMDP.FiniteHorizon.robust_dynamic_programming

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programminggame-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Consider a finite-horizon MDP with states $\mathcal X=\{1,\dots,n\}$ , horizon $T=\{0,\dots,N-1\}$ , a finite nonempty action set $\mathcal A$ , nonnegative stage costs $c_t(i,a)$ , a terminal cost $c_N$ , an initial state $i_0$ , and rectangular uncertainty: nonempty sets $\mathcal P_i^a\subseteq\Delta_n$ of possible $i$ -th rows of the transition matrix under action $a$ (no other assumption). Let $\Pi$ be the deterministic Markov controller policies, $\mathcal T$ the admissible time-varying policies of nature, and $C_N(\pi,\tau)$ the expected total cost (2). Let $v$ be given by the robust recursion (7) and, for $\pi\in\Pi$ , $v^\pi$ by recursion (10), both with terminal value $c_N$ . Then:

Perfect duality holds, with value given by (7):

\varphi_N(\Pi,\mathcal T)=\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau)=\psi_N(\Pi,\mathcal T).

For every $\pi\in\Pi$ , the worst-case cost is given by (10): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$ .
Every policy $\pi^*=(\mathbf a_0^*,\dots,\mathbf a_{N-1}^*)$ with $\mathbf a_t^*(i)\in\arg\min_{a\in\mathcal A}\{c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\}$ for all $t,i$ (rule (8)) is optimal: $\sup_{\tau\in\mathcal T}C_N(\pi^*,\tau)=v_0(i_0)$ .
Every policy of nature $\tau^*$ whose rows satisfy $p_i^a(t)\in\arg\max\{p^{\mathsf T}v_{t+1}:p\in\mathcal P_i^a\}$ for all $t,a,i$ (rule (9)) is a worst case: $\min_{\pi\in\Pi}C_N(\pi,\tau^*)=v_0(i_0)$ , and $C_N(\pi^*,\tau^*)=v_0(i_0)$ for every $\pi^*$ as in 3.

The theorem says that the robust control problem with time-varying rectangular uncertainty is solved by a dynamic programming recursion of the same form as the nominal one, with the expected continuation cost replaced by a support function, and that the order of play between controller and nature does not matter. Convexity of the uncertainty sets is not required.

Formalization Note $\Pi$ is finite and nonempty, so minima over it are Lean's ⨅. The paper writes "max" over nature; the row sets need not be closed, so these are suprema ⨆ over the nonempty set $\mathcal T$ , whose costs are bounded above because every row lies in $\Delta_n$ . For the same reason the maxima in (9) need not be attained, and conclusion 4 is stated for nature policies that attain them. The argmin rule (8) is stated for every policy attaining the minimum, not a particular choice. The terminal value $v_N=c_N$ is implicit in the paper's proof and explicit on p. 785. The paper's " $(\mathbf a_0,\dots,\mathbf a_N)$ " in the sentence before (10) is read as $(\mathbf a_0,\dots,\mathbf a_{N-1})$ .

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Shared_supportFunction
import Definitions.Def_RobustMDP_FiniteHorizon_Model
import Definitions.Def_RobustMDP_FiniteHorizon_expectedCost
import Definitions.Def_RobustMDP_FiniteHorizon_robustValue

Formal statement

namespace RobustMDP.FiniteHorizon

/-- Theorem 1 (Robust Dynamic Programming), Nilim–El Ghaoui 2005, pp. 782–783.
For a finite-horizon MDP with rectangular uncertainty (nonempty row sets `𝒫_i^a ⊆ Δ_n`, no other
assumption), initial state `i₀`, and `C_N(π, τ)` the expected total cost (2):

1. perfect duality holds, with value given by recursion (7):
   `min_{π ∈ Π} sup_{τ ∈ 𝒯} C_N(π, τ) = v_0(i₀) = sup_{τ ∈ 𝒯} min_{π ∈ Π} C_N(π, τ)`;
2. for every policy `π`, the worst case `sup_{τ ∈ 𝒯} C_N(π, τ)` is `v_0^π(i₀)`, recursion (10);
3. every policy `π*` whose actions attain the minimum in (8),
   `𝐚*_t(i) ∈ argmin_a {c_t(i, a) + σ_{𝒫_i^a}(v_{t+1})}`, is optimal:
   `sup_{τ ∈ 𝒯} C_N(π*, τ) = v_0(i₀)`;
4. every nature policy `τ*` whose rows attain the maxima in (9),
   `p_i^a(t) ∈ argmax {pᵀ v_{t+1} : p ∈ 𝒫_i^a}`, is a worst case:
   `min_{π ∈ Π} C_N(π, τ*) = v_0(i₀)`, and `C_N(π*, τ*) = v_0(i₀)` for every `π*` as in 3.

`Π` is finite, so its minima are `⨅`; nature's maxima are `⨆` over the (possibly infinite) set
`𝒯`, which is nonempty and whose costs are bounded above. The row maxima of (9) need not be
attained, so conclusion 4 is stated for nature policies that attain them. -/
theorem robust_dynamic_programming {n N : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n N A) (i₀ : Fin n) :
    ((⨅ π : ControlPolicy n N A, ⨆ τ : M.NaturePolicy, M.expectedCost i₀ π τ.1) =
        M.robustValue 0 i₀ ∧
      (⨆ τ : M.NaturePolicy, ⨅ π : ControlPolicy n N A, M.expectedCost i₀ π τ.1) =
        M.robustValue 0 i₀) ∧
    (∀ π : ControlPolicy n N A,
      (⨆ τ : M.NaturePolicy, M.expectedCost i₀ π τ.1) = M.policyValue π 0 i₀) ∧
    (∀ πstar : ControlPolicy n N A,
      (∀ (t : Fin N) (i : Fin n) (a : A),
        M.cost t i (πstar t i) + Shared.supportFunction (M.rows (πstar t i) i) (M.robustValue (t + 1)) ≤
          M.cost t i a + Shared.supportFunction (M.rows a i) (M.robustValue (t + 1))) →
      (⨆ τ : M.NaturePolicy, M.expectedCost i₀ πstar τ.1) = M.robustValue 0 i₀) ∧
    (∀ τstar : M.NaturePolicy,
      (∀ (t : Fin N) (a : A) (i : Fin n),
        ∑ j, τstar.1 t a i j * M.robustValue (t + 1) j =
          Shared.supportFunction (M.rows a i) (M.robustValue (t + 1))) →
      (⨅ π : ControlPolicy n N A, M.expectedCost i₀ π τstar.1) = M.robustValue 0 i₀ ∧
      ∀ πstar : ControlPolicy n N A,
        (∀ (t : Fin N) (i : Fin n) (a : A),
          M.cost t i (πstar t i) + Shared.supportFunction (M.rows (πstar t i) i) (M.robustValue (t + 1)) ≤
            M.cost t i a + Shared.supportFunction (M.rows a i) (M.robustValue (t + 1))) →
        M.expectedCost i₀ πstar τstar.1 = M.robustValue 0 i₀) := by sorry

end RobustMDP.FiniteHorizon

Source

Nilim and El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Oper. Res. 53 (2005), pp. 782–783, Theorem 1

Read-back

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

Setting. The statement fixes the following:

natural numbers $n$ (the number of states) and $N$ (the horizon);
a type $A$ of actions, which must be finite and nonempty;
a model $M$ of type "finite-horizon robust MDP with $n$ states, horizon $N$ and actions $A$ ";
an initial state $i_0 \in \{0,\dots,n-1\}$ .

The code uses several named notions: $M$ 's stage costs, its uncertainty sets (called "rows"), its set of nature policies, the expected cost, the robust value, the policy value, and a support function. Their definitions are in imported files that are not part of the supplied code, so they cannot be unfolded here. Only the following can be read off from how they are used:

Control policy $\pi$ . It assigns an action $\pi_t(i) \in A$ to each stage $t \in \{0,\dots,N-1\}$ and state $i$ . The minima below range over the whole type of control policies.
Nature policy $\tau$ . It is an element of a set $\mathcal T_M$ defined by the model; the membership condition is hidden. Its underlying data $\tau_t(a,i,j)$ is a number for each stage $t$ , action $a$ , state $i$ and next state $j$ .
Stage cost. $c_t(i,a)$ is a number.
Uncertainty set. $\mathcal P^{a}_{i}$ ( $M$ 's "rows" at action $a$ , state $i$ ) is passed to a support function $\sigma_{\mathcal P}(v)$ , which also takes a vector $v$ indexed by states.
Values. The following appear:
- the expected cost $C_N(i_0,\pi,\tau)$ , evaluated on the underlying data of $\tau$ ;
- the robust value $v_s(i)$ at stage $s$ and state $i$ ;
- the policy value $v^\pi_s(i)$ .

The theorem asserts the conjunction of four statements.

Two dualities.

\inf_{\pi}\ \sup_{\tau\in\mathcal T_M} C_N(i_0,\pi,\tau) = v_0(i_0) \qquad\text{and}\qquad \sup_{\tau\in\mathcal T_M}\ \inf_{\pi} C_N(i_0,\pi,\tau) = v_0(i_0).

Worst case of each policy. For every control policy $\pi$ :

\sup_{\tau\in\mathcal T_M} C_N(i_0,\pi,\tau) = v^\pi_0(i_0).

Greedy policies are optimal. Take any control policy $\pi^*$ such that, for every stage $t\in\{0,\dots,N-1\}$ , every state $i$ and every action $a\in A$ ,

c_t\big(i,\pi^*_t(i)\big) + \sigma_{\mathcal P^{\pi^*_t(i)}_{i}}\big(v_{t+1}\big) \;\le\; c_t(i,a) + \sigma_{\mathcal P^{a}_{i}}\big(v_{t+1}\big).

Then

\sup_{\tau\in\mathcal T_M} C_N(i_0,\pi^*,\tau) = v_0(i_0).

The condition must hold at all states, not only the ones reachable from $i_0$ .

Attaining nature policies are worst cases. Take any nature policy $\tau^*\in\mathcal T_M$ such that, for every stage $t\in\{0,\dots,N-1\}$ , every action $a$ and every state $i$ ,

\sum_{j} \tau^*_t(a,i,j)\, v_{t+1}(j) = \sigma_{\mathcal P^{a}_{i}}\big(v_{t+1}\big).

Then both of the following hold:

$\inf_{\pi} C_N(i_0,\pi,\tau^*) = v_0(i_0)$ ;
$C_N(i_0,\pi^*,\tau^*) = v_0(i_0)$ for every $\pi^*$ that satisfies the condition in item 3.

The condition is an equation between the $v_{t+1}$ -weighted sum of $\tau^*$ 's row and the support-function value. Whether that row lies in $\mathcal P^a_i$ is not stated here; it holds only if the hidden membership condition of $\mathcal T_M$ imposes it.

Fine print.

Stage index. In items 3 and 4, $t$ lies in $\{0,\dots,N-1\}$ and the next stage is written $t+1$ . The code does not show what type the robust value's stage argument has. If it is a natural number, $t+1$ is the ordinary successor, reaching $N$ at the last stage. If the addition happens in $\{0,\dots,N-1\}$ , then $t+1$ wraps around to $0$ when $t=N-1$ .
No explicit hypotheses on the model. Nothing in the statement says:
- that the uncertainty sets are nonempty or bounded;
- that $\mathcal T_M$ is nonempty;
- that the costs $C_N(i_0,\pi,\cdot)$ are bounded above over $\mathcal T_M$ .
Any such property would have to come from the hidden definition of the model. If the values are real numbers (the use of $+$ , $\le$ and finite sums suggests so, but the type is not shown), then a supremum over an empty set, or over a set that is not bounded above, takes the conventional value $0$ . The same would apply to a support function taken over such a set. In those cases the equalities above compare such default values with $v_0(i_0)$ or $v^\pi_0(i_0)$ .
Infima over policies. These range over a type that is finite and nonempty whenever it consists of stage-and-state-indexed action choices, since $A$ is finite and nonempty. In that case each infimum is an attained minimum.

Degenerate cases.

$n=0$ . There is no initial state $i_0$ , so the theorem is vacuous.
$N=0$ . There are no stages, so the conditions in items 3 and 4 hold vacuously. Every control policy then counts as $\pi^*$ and every element of $\mathcal T_M$ counts as $\tau^*$ . The theorem then asserts, for every $\pi$ and every $\tau\in\mathcal T_M$ :

C_0(i_0,\pi,\tau) = v_0(i_0), \qquad \sup_{\tau} C_0(i_0,\pi,\tau) = v_0(i_0) = v^\pi_0(i_0),

with the supremum taking whatever default value applies if $\mathcal T_M$ is empty.

One action. If $A$ has a single element, the condition in item 3 holds trivially, so the unique policy is asserted to satisfy item 3's conclusion.
Empty $\mathcal T_M$ . Item 4 is vacuous. Item 1's second equality and items 2 and 3 then equate the empty supremum (its default value, e.g. $0$ in the reals) with $v_0(i_0)$ and $v^\pi_0(i_0)$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph