Proof of Theorem 1, p. 783 — the maps $g_t$ of problems (15) and (16) are componentwise nondecreasing

Proved

RobustMDP.FiniteHorizon.bellman_maps_monotone

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$ . For each stage $t\in T$ define $g_t:\mathbb R^n\to\mathbb R^n$ componentwise, for problem (15), by

(g_t(v))_i:=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v)\big),\qquad i\in\mathcal X,

and, for a controller policy $\pi=(\mathbf a_t)_{t\in T}$ and problem (16), by

(g_t(v))_i:=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v),\qquad i\in\mathcal X .

Both maps are componentwise nondecreasing, for every $t$ and every $\pi$ .

This is the hypothesis of Lemma 1 for problems (15) and (16), which yields recursions (7) and (10).

Formalization Note The minimum over the finite nonempty action set is Lean's ⨅ a.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Shared_supportFunction
import Definitions.Def_RobustMDP_FiniteHorizon_Model

Formal statement

namespace RobustMDP.FiniteHorizon

/-- (p. 783, proof of Theorem 1.) For every stage `t`, the maps `g_t : ℝⁿ → ℝⁿ` defined by
`(g_t(v))_i := min_{a ∈ 𝒜} (c_t(i, a) + σ_{𝒫_i^a}(v))` (for problem (15)) and, for every
controller policy `π`, `(g_t(v))_i := c_t(i, 𝐚_t(i)) + σ_{𝒫_i^{𝐚_t(i)}}(v)` (for problem (16))
are componentwise nondecreasing. The minimum over the finite nonempty action set is `⨅ a`. -/
theorem bellman_maps_monotone {n N : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n N A) (t : Fin N) :
    Monotone (fun (v : Fin n → ℝ) (i : Fin n) =>
      ⨅ a : A, (M.cost t i a + Shared.supportFunction (M.rows a i) v)) ∧
    ∀ π : ControlPolicy n N A,
      Monotone (fun (v : Fin n → ℝ) (i : Fin n) =>
        M.cost t i (π t i) + Shared.supportFunction (M.rows (π t i) i) v) := 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, proof of Theorem 1, definitions of g_t for (15) and (16)

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 and $M$ a model with $n$ states and $N$ stages. So $M$ has:

stage costs $c_t(i,a) \ge 0$ ;
terminal costs $c_N(i)$ ;
nonempty row sets $\mathcal{P}_i^a$ inside the standard simplex.

Fix a stage $t < N$ . As before, $\sigma_S$ denotes the imported function Shared.supportFunction, whose definition is not shown.

Conclusion. Two statements hold at this stage.

The map $G_t : \mathbb{R}^n \to \mathbb{R}^n$ given by

G_t(v)_i = \min_{a \in A}\big(c_t(i,a) + \sigma_{\mathcal{P}_i^a}(v)\big)

is monotone: $u \le v$ componentwise implies $G_t(u) \le G_t(v)$ componentwise. The minimum is written as a real infimum, and it is a genuine minimum because $A$ is finite and nonempty. 2. For every control policy $\pi$ , the map

v \mapsto \Big(c_t(i,\pi_t(i)) + \sigma_{\mathcal{P}_i^{\pi_t(i)}}(v)\Big)_{i}

is monotone in the same sense.

Degenerate cases.

$N = 0$ : no stage $t$ exists, so the statement is vacuous.
$n = 0$ : both maps go into the zero-dimensional space and are trivially monotone.

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

Proof of Theorem 1, p. 783 — the maps gtg_tgt​ of problems (15) and (16) are componentwise nondecreasing

Proof of Theorem 1, p. 783 — the maps $g_t$ of problems (15) and (16) are componentwise nondecreasing