Eqs. (28) and (23), pp. 785–786 — the worst-case cost of a stationary policy solves the robust evaluation equation

Proved

RobustMDP.Discounted.worstCase_policy_eval

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

dynamic-programmingmarkov-decision-processp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Fix an initial state $i_0$ and a stationary control policy $\pi = (\mathbf a, \mathbf a, \dots)$ . The equation

v^\pi(i) = c(i, \mathbf a(i)) + \nu\, \sigma_{\mathcal P_i^{\mathbf a(i)}}(v^\pi), \qquad i \in \mathcal X, \tag{23}

has exactly one solution $v^\pi \in \mathbb R^n$ , and the worst-case discounted cost of $\pi$ over stationary policies of nature is

\phi_\infty(\pi, \mathcal T_s) = \sup_{\tau \in \mathcal T_s} C_\infty(\pi, \tau) = v^\pi(i_0).

In the paper this value is the optimum of the nonlinear program (28), obtained from (26) by letting nature's matrices become variables; (23) is its characterization.

Formalization Note The paper writes $\max_{\tau \in \mathcal T_s}$ . The row sets need not be closed, so the supremum need not be attained, and it is stated as a least upper bound (IsLUB) of the set of costs $C_\infty(\pi, \tau)$ , $\tau \in \mathcal T_s$ .

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Discounted_Model
import Definitions.Def_RobustMDP_Shared_supportFunction
import Definitions.Def_RobustMDP_Discounted_discountedCost
import Definitions.Def_RobustMDP_Discounted_bellmanOps

Formal statement

namespace RobustMDP.Discounted

/-- Problem (28) and equation (23) (Nilim–El Ghaoui 2005, pp. 785–786). For every stationary
controller policy `π = (𝐚, 𝐚, …)`, the equation (23)
`v^π(i) = c(i, 𝐚(i)) + ν σ_{𝒫_i^{𝐚(i)}}(v^π)`, `i ∈ 𝒳`, has exactly one solution `v^π ∈ ℝⁿ`,
and the worst-case discounted cost `φ_∞(π, 𝒯_s) = sup_{P ∈ 𝒯_s} C_∞(π, P)` from the initial
state `i₀` equals `v^π(i₀)`. The supremum over the (generally infinite) set `𝒯_s` is stated as a
least upper bound, since it need not be attained. -/
theorem worstCase_policy_eval {n : ℕ} {A : Type} (M : Model n A) (i₀ : Fin n)
    (π : StationaryPolicy n A) :
    ∃ vπ : Fin n → ℝ,
      M.policyOp π vπ = vπ ∧ (∀ w, M.policyOp π w = w → w = vπ) ∧
      IsLUB (Set.range fun P : M.StationaryNature => M.discountedCost i₀ π P) (vπ i₀) := by sorry

end RobustMDP.Discounted

Source

Nilim and El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Oper. Res. 53 (2005), p. 786, Eq. (28); p. 785, Theorem 3, Eq. (23)

Read-back

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

The inputs are any model $M$ (with $A$ arbitrary, not required to be finite), an initial state $i_0$ , and a stationary policy $\pi$ . The statement asserts that there exists $v^\pi \in \mathbb{R}^n$ with three properties:

$v^\pi = g_\pi(v^\pi)$ . Written out:

v^\pi(i) = c\big(i,\pi(i)\big) + \nu\,\sigma_{\mathcal{P}_i^{\pi(i)}}(v^\pi) \quad \text{for all } i,

where $\sigma$ is an externally defined quantity not shown here. 2. Every $w$ with $g_\pi(w) = w$ equals $v^\pi$ . 3. $v^\pi(i_0)$ is the least upper bound of $\{ C_\infty(\pi,P) : P \text{ a stationary nature policy of } M\}$ .

Here $C_\infty$ is the discounted cost from $i_0$ . Property 3 means two things:

$C_\infty(\pi,P) \le v^\pi(i_0)$ for every nature policy $P$ ;
no smaller number is an upper bound.

It does not assert that some $P$ attains the value. The set of nature policies is nonempty because every row set is nonempty.

Degenerate cases:

$n = 0$ : no $i_0$ exists, so the statement is vacuous.
$\nu = 0$ : the claim becomes $v^\pi(i) = c(i,\pi(i))$ , and the supremum of the constant $c(i_0,\pi(i_0))$ equals it.

Human review

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

View graph