Eqs. (27) and (19), pp. 785–786 — the max–min value $\psi_\infty(\Pi_s, \mathcal T_s)$ solves the robust Bellman equation

Proved

RobustMDP.Discounted.maxmin_value

by mikedeng1 · Sep 28, 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$ . The robust Bellman equation

v(i) = \min_{a \in \mathcal A} \big(c(i, a) + \nu\, \sigma_{\mathcal P_i^a}(v)\big), \qquad i \in \mathcal X, \tag{19}

has exactly one solution $v \in \mathbb R^n$ , and the max–min value of the game between nature and the controller over stationary policies is

\psi_\infty(\Pi_s, \mathcal T_s) = \sup_{\tau \in \mathcal T_s} \min_{\pi \in \Pi_s} C_\infty(\pi, \tau) = v(i_0).

In the paper this value is the optimum of the nonlinear program (27), obtained from the linear program (25) of the nominal problem by letting nature's matrices become variables.

Formalization Note The minimum over the finite set $\Pi_s$ is ⨅. The paper writes $\max_{\tau}$ ; the row sets need not be closed, so the outer supremum is stated as a least upper bound (IsLUB).

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 (27) and equation (19) (Nilim–El Ghaoui 2005, pp. 785–786). The equation (19)
`v(i) = min_{a ∈ 𝒜} (c(i, a) + ν σ_{𝒫_i^a}(v))`, `i ∈ 𝒳`, has exactly one solution `v ∈ ℝⁿ`,
and the max–min value `ψ_∞(Π_s, 𝒯_s) = sup_{P ∈ 𝒯_s} min_{π ∈ Π_s} C_∞(π, P)` from the initial
state `i₀` equals `v(i₀)`. The inner minimum over the finite set `Π_s` is `⨅`; the outer supremum
over the (generally infinite) set `𝒯_s` is stated as a least upper bound. -/
theorem maxmin_value {n : ℕ} {A : Type} [Fintype A] [Nonempty A] (M : Model n A) (i₀ : Fin n) :
    ∃ v : Fin n → ℝ,
      M.bellmanOp v = v ∧ (∀ w, M.bellmanOp w = w → w = v) ∧
      IsLUB (Set.range fun P : M.StationaryNature =>
          ⨅ π : StationaryPolicy n A, 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. (27); p. 785, Theorem 3, Eq. (19)

Read-back

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

The inputs are a finite nonempty action type $A$ , any model $M$ , and an initial state $i_0$ . The statement asserts that there exists $v \in \mathbb{R}^n$ with three properties:

$g(v) = v$ . Written out:

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

where $\sigma$ is an externally defined quantity not shown here. 2. Every $w$ with $g(w) = w$ equals $v$ . 3. $v(i_0)$ is the least upper bound, over all stationary nature policies $P$ of $M$ , of the quantity

\min_{\pi} C_\infty(\pi, P),

the minimum of the discounted cost from $i_0$ over all stationary policies $\pi : \{0,\dots,n-1\}\to A$ .

The inner infimum is over a finite nonempty set (there are $|A|^n \ge 1$ policies), so it is a genuine minimum. The outer value is a supremum: it is an upper bound of the set, and no smaller number is. It is not asserted to be attained by any $P$ .

Degenerate cases:

$n = 0$ : no $i_0$ exists, so the statement is vacuous.
$\nu = 0$ : the claim is $v(i) = \min_a c(i,a)$ , and $v(i_0) = \min_\pi c(i_0,\pi(i_0))$ .
$|A| = 1$ : there is a single policy, and the claim reduces to a worst-case evaluation of that policy.

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

Eqs. (27) and (19), pp. 785–786 — the max–min value ψ∞(Πs,Ts)\psi_\infty(\Pi_s, \mathcal T_s)ψ∞​(Πs​,Ts​) solves the robust Bellman equation

Eqs. (27) and (19), pp. 785–786 — the max–min value $\psi_\infty(\Pi_s, \mathcal T_s)$ solves the robust Bellman equation