Step (e), p. 787 — $\phi_N(\Pi,\mathcal T_s)\to\phi_\infty(\Pi,\mathcal T_s)$ at geometric rate $\nu$

Proved

RobustMDP.Stationarity.stationaryUncertainty_value_converges

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

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

In a robust discounted MDP with discount factor $0<\nu<1$ (finite states, finite nonempty action set, costs $c\ge0$ , nonempty rectangular row sets in the simplex), for every horizon $N$

\phi_N(\Pi,\mathcal T_s)\le\phi_\infty(\Pi,\mathcal T_s)\le\phi_N(\Pi,\mathcal T_s)+\varepsilon_N,\qquad \varepsilon_N=\frac{\nu^N c_{\max}}{1-\nu},

where $\phi_N(\Pi,\mathcal T_s)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal T_s}C_N(\pi,\tau)$ is the robust value when nature must use the same transition matrices at every stage, and $\phi_\infty(\Pi,\mathcal T_s)$ its infinite-horizon counterpart.

Together with Eq. (35) this bounds the gap between time-varying and stationary uncertainty in Theorem 4.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Stationarity_Model
import Definitions.Def_RobustMDP_Stationarity_gameValues

Formal statement

namespace RobustMDP.Stationarity

/-- Nilim–El Ghaoui 2005, p. 787, Step (e): for every `N`,
`φ_N(Π, 𝒯_s) ≤ φ_∞(Π, 𝒯_s) ≤ φ_N(Π, 𝒯_s) + ε_N`. -/
theorem stationaryUncertainty_value_converges {n : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n A) (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) (N : ℕ) :
    M.phiN_PTs ν i₀ N ≤ M.phiInf_PTs ν i₀ ∧
      M.phiInf_PTs ν i₀ ≤ M.phiN_PTs ν i₀ N + M.epsN ν N := by sorry

end RobustMDP.Stationarity

Source

Nilim and El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Oper. Res. 53 (2005), p. 787, proof of Theorem 4, Step (e), first display

Read-back

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

Setting. Let $n\in\mathbb N$ with states $\{0,\dots,n-1\}$ , and let $A$ be a finite, nonempty action set. The model gives:

costs $c(i,a)\ge0$ ;
nonempty sets $\mathcal P_i^a$ of probability vectors on the states. No convexity or closedness is assumed.

Let $0<\nu<1$ and let $i_0$ be an initial state.

A controller policy $\pi=(\pi_t)_{t\in\mathbb N}$ is a sequence of maps from states to actions.
A choice of nature $P=(P^a)_{a\in A}$ is a family of matrices with rows $P^a(i,\cdot)\in\mathcal P_i^a$ . It is used at every time step, as the constant nature policy $(P,P,\dots)$ .

The state distribution is $\mu_0=e_{i_0}$ , $\mu_{t+1}(j)=\sum_i\mu_t(i)P^{\pi_t(i)}(i,j)$ . The costs are

C_N(\pi,P)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)c(i,\pi_t(i)),

and $C_\infty(\pi,P)$ is the infinite sum, which is summable here.

The two values compared are

\varphi_N=\inf_{\pi}\sup_{P}C_N(\pi,P),\qquad \varphi_\infty=\inf_{\pi}\sup_{P}C_\infty(\pi,P).

The infima range over all (possibly time-varying) controller policies, and the suprema over single choices of nature held fixed through time. Finally $\varepsilon_N=\nu^Nc_{\max}/(1-\nu)$ with $c_{\max}=\max_{i,a}c(i,a)$ .

Claim. For every $N\in\mathbb N$ :

\varphi_N\;\le\;\varphi_\infty\;\le\;\varphi_N+\varepsilon_N.

Degenerate cases.

$n=0$ : no initial state exists, so the statement is vacuous.
$N=0$ : $\varphi_0=0$ , and the claim becomes $0\le\varphi_\infty\le c_{\max}/(1-\nu)$ .
Real conventions: all quantities are bounded in $[0,c_{\max}/(1-\nu)]$ and all index sets are nonempty, so the real-supremum and real-infimum conventions for empty or unbounded families do not arise.
Single-element sets: if every $\mathcal P_i^a$ has one element, there is only one choice of nature, and the supremum is trivial.

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

Step (e), p. 787 — ϕN(Π,Ts)→ϕ∞(Π,Ts)\phi_N(\Pi,\mathcal T_s)\to\phi_\infty(\Pi,\mathcal T_s)ϕN​(Π,Ts​)→ϕ∞​(Π,Ts​) at geometric rate ν\nuν

Step (e), p. 787 — $\phi_N(\Pi,\mathcal T_s)\to\phi_\infty(\Pi,\mathcal T_s)$ at geometric rate $\nu$