Eq. (16), p. 783 — the worst-case cost of a fixed policy is given by recursion (10)

Proved

RobustMDP.FiniteHorizon.worstCase_policy_recursion

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

dynamic-programmingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Consider a finite-horizon robust MDP with nonempty row sets $\mathcal P_i^a\subseteq\Delta_n$ , an initial state $i_0$ and a controller policy $\pi$ . The worst-case expected total cost of $\pi$ over all admissible policies of nature,

\varphi_N(\pi,\mathcal T)=\sup_{\tau\in\mathcal T}C_N(\pi,\tau),

equals $v_0^\pi(i_0)$ , where $v^\pi$ is computed by recursion (10): $v_N^\pi=c_N$ and $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$ .

This is the paper's problem (16) solved by Lemma 1: the rectangular structure of $\mathcal T$ lets nature optimise each row separately, which is where the support functions come from.

Formalization Note The paper writes "max"; since the sets $\mathcal P_i^a$ need not be closed, the worst case is a supremum, stated as a least upper bound (IsLUB) of the set of costs $\{C_N(\pi,\tau):\tau\in\mathcal T\}$ .

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

/-- Problem (16), p. 783, solved by recursion (10). For every controller policy `π`, the
worst-case expected total cost `φ_N(π, 𝒯) = sup_{τ ∈ 𝒯} C_N(π, τ)` over all admissible
(time-varying, rectangular) policies of nature is the value `v_0^π(i₀)` of the recursion
`v_t^π(i) = c_t(i, 𝐚_t(i)) + σ_{𝒫_i^{𝐚_t(i)}}(v_{t+1}^π)`, `v_N^π = c_N`. The paper's "max"
is stated as a least upper bound, since the row sets need not be closed. -/
theorem worstCase_policy_recursion {n N : ℕ} {A : Type} (M : Model n N A) (i₀ : Fin n)
    (π : ControlPolicy n N A) :
    IsLUB (Set.range fun τ : M.NaturePolicy => M.expectedCost i₀ π τ.1)
      (M.policyValue π 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), p. 783, Eq. (16) and the paragraph after it; Theorem 1, Eq. (10)

Read-back

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

Hypotheses. The statement fixes:

a model $M$ with $n$ states, $N$ stages and any action type $A$ (not assumed finite or nonempty), with stage costs $c_t \ge 0$ , terminal cost $c_N$ , and nonempty row sets $\mathcal{P}_i^a \subseteq \Delta_n$ ;
an initial state $i_0$ ;
a control policy $\pi$ .

Conclusion. The number $v^\pi_0(i_0)$ is the least upper bound of the set

\{\,C_N(\pi,\tau) : \tau \text{ a nature policy of } M\,\}.

The objects in this statement are:

Nature policy $\tau$ : any array whose row $\tau_t^a(i,\cdot)$ lies in $\mathcal{P}_i^a$ for every stage $t$ , action $a$ and state $i$ , chosen independently for each triple.
Expected cost $C_N(\pi,\tau)$ : the cost defined earlier, computed from the forward distributions $\mu_{t+1}(j)=\sum_i \mu_t(i)\,\tau_t^{\pi_t(i)}(i,j)$ with $\mu_0$ the point mass at $i_0$ .
Value $v^\pi$ : $v^\pi_N = c_N$ and $v^\pi_t(i) = c_t(i,\pi_t(i)) + \sigma_{\mathcal{P}_i^{\pi_t(i)}}(v^\pi_{t+1})$ , where $\sigma$ is the imported, unshown Shared.supportFunction.

"Least upper bound" means $v^\pi_0(i_0) \ge C_N(\pi,\tau)$ for every $\tau$ , and no smaller number has this property. The bound need not be attained by any $\tau$ . Since a least upper bound in $\mathbb{R}$ is asserted, the statement also implies that the set is bounded above.

Degenerate cases.

$N = 0$ : the only nature policy is the empty one. The set is $\{c_N(i_0)\}$ and $v^\pi_0(i_0) = c_N(i_0)$ .
$n = 0$ : there is no $i_0$ , so the statement has no instances.
$A$ empty and $N>0$ (with $n>0$ ): no $\pi$ exists, so the statement is vacuous.

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