Eq. (15), p. 783 — the max–min value $\psi_N(\Pi,\mathcal T)$ is given by recursion (7)

Proved

RobustMDP.FiniteHorizon.maxmin_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$ and an initial state $i_0$ . The max–min value, in which nature commits to $\tau\in\mathcal T$ and the controller then chooses a policy,

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

equals $v_0(i_0)$ , where $v$ is computed by the robust recursion (7): $v_N=c_N$ and $v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big)$ .

This is the paper's problem (15), a nonlinear program in the value functions and the transition matrices, solved by Lemma 1 thanks to rectangularity. Together with weak duality and recursion (10) it gives the perfect duality of Theorem 1.

Formalization Note $\Pi$ is finite and nonempty, so the inner minimum is Lean's ⨅ π. The paper's "max" over nature is a supremum, since the row sets need not be closed; it is stated as a least upper bound (IsLUB).

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 (15), p. 783, solved by recursion (7). The max–min value
`ψ_N(Π, 𝒯) = sup_{τ ∈ 𝒯} min_{π ∈ Π} C_N(π, τ)` (nature moves first, the controller responds
with a deterministic Markov policy) equals the value `v_0(i₀)` of the robust recursion
`v_t(i) = min_{a ∈ 𝒜} (c_t(i, a) + σ_{𝒫_i^a}(v_{t+1}))`, `v_N = c_N`. The minimum over the
finite nonempty set `Π` is `⨅ π`; the paper's "max" over nature is stated as a least upper
bound, since the row sets need not be closed. -/
theorem maxmin_recursion {n N : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n N A) (i₀ : Fin n) :
    IsLUB (Set.range fun τ : M.NaturePolicy => ⨅ π : ControlPolicy n N A, M.expectedCost i₀ π τ.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), p. 783, Eq. (15) and the paragraph after (16); Theorem 1, Eq. (7)

Read-back

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

Hypotheses. Let $A$ be a finite, nonempty set of actions. Let $M$ be a model with $n$ states and $N$ stages, with stage costs $c_t \ge 0$ , terminal cost $c_N$ , and nonempty row sets $\mathcal{P}_i^a \subseteq \Delta_n$ . Fix an initial state $i_0$ .

Conclusion. The number $v_0(i_0)$ is the least upper bound of the set

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

The objects in this statement are:

Nature policy $\tau$ : its rows satisfy $\tau_t^a(i,\cdot) \in \mathcal{P}_i^a$ , chosen independently for each stage $t$ , action $a$ and state $i$ .
The inner minimum: it ranges over all deterministic Markov control policies $\pi$ , meaning all functions from pairs (stage, state) to $A$ . It is written as a real infimum, but it is a genuine minimum because this set of policies is finite and nonempty. The policy $\pi$ is chosen after, and with knowledge of, the entire $\tau$ .
Expected cost $C_N(\pi,\tau)$ : as defined earlier, with $\mu_0$ the point mass at $i_0$ and $\mu_{t+1}(j) = \sum_i \mu_t(i)\,\tau_t^{\pi_t(i)}(i,j)$ .
Value $v$ : $v_N = c_N$ and $v_t(i) = \min_{a\in A}\big(c_t(i,a) + \sigma_{\mathcal{P}_i^a}(v_{t+1})\big)$ , where $\sigma$ is the imported, unshown Shared.supportFunction.

"Least upper bound" means $v_0(i_0)$ bounds every member of the set, and no smaller number does. It need not be attained by any $\tau$ .

Degenerate cases.

$N = 0$ : there is exactly one policy and one nature policy. The set is $\{c_N(i_0)\}$ and $v_0(i_0) = c_N(i_0)$ .
$n = 0$ : there is no $i_0$ , so the statement has no instances.
$A$ with one element: there is a single control policy, and the statement reduces to a worst case over nature alone.

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

Eq. (15), p. 783 — the max–min value ψN(Π,T)\psi_N(\Pi,\mathcal T)ψN​(Π,T) is given by recursion (7)

Eq. (15), p. 783 — the max–min value $\psi_N(\Pi,\mathcal T)$ is given by recursion (7)