Eq. (33), p. 786 — the finite-horizon robust value converges to the stationary game value $\phi_\infty(\Pi_s,\mathcal T_s)$

Proved

RobustMDP.Stationarity.finiteHorizon_converges_to_stationary

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

dynamic-programmingmarkov-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 $\varepsilon>0$ there is $N_\varepsilon$ such that for every $N>N_\varepsilon$

\phi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\le\phi_N(\Pi,\mathcal T)\le\phi_\infty(\Pi_s,\mathcal T_s).

In particular the finite-horizon robust value under time-varying uncertainty, $\phi_N(\Pi,\mathcal T)$ , converges to the value of the stationary infinite-horizon game (6).

This is Step (a) of the proof of Theorem 4; combined with Eq. (35) it yields $\phi_\infty(\Pi,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$ .

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. 786, Step (a), Eq. (33): for every `ε > 0` there is `N_ε` such that
for every `N > N_ε`, `φ_∞(Π_s, 𝒯_s) - ε ≤ φ_N(Π, 𝒯) ≤ φ_∞(Π_s, 𝒯_s)`; in particular
`φ_N(Π, 𝒯) → φ_∞(Π_s, 𝒯_s)`. -/
theorem finiteHorizon_converges_to_stationary {n : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n A) (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) :
    ∀ ε > 0, ∃ Nε : ℕ, ∀ N > Nε,
      M.phiInf_PsTs ν i₀ - ε ≤ M.phiN_PT ν i₀ N ∧ M.phiN_PT ν i₀ N ≤ M.phiInf_PsTs ν i₀ := 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. 786, Eq. (33) (proof of Theorem 4, Step (a))

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 nature policy $\tau=(P_t)_{t\in\mathbb N}$ is a sequence of matrix families $(P_t^a)_{a\in A}$ with rows $P_t^a(i,\cdot)\in\mathcal P_i^a$ .

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

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

and $C_\infty$ is the infinite sum, which is summable here.

The two values compared are

\varphi_N(\Pi,\mathcal T)=\inf_{\pi}\sup_{\tau}C_N(\pi,\tau),

over all controller and nature policies, and

\varphi_\infty(\Pi_s,\mathcal T_s)=\inf_{\sigma}\sup_{P}C_\infty\big((\sigma,\sigma,\dots),(P,P,\dots)\big),

over single maps $\sigma$ from states to actions and single choices of nature $P$ , each used at every time.

Claim. For every $\varepsilon>0$ there is $N_\varepsilon\in\mathbb N$ such that every $N>N_\varepsilon$ satisfies

\varphi_\infty(\Pi_s,\mathcal T_s)-\varepsilon\;\le\;\varphi_N(\Pi,\mathcal T)\;\le\;\varphi_\infty(\Pi_s,\mathcal T_s).

Both inequalities are asserted only for $N>N_\varepsilon$ , not for every $N$ . In particular, $\varphi_N(\Pi,\mathcal T)\to\varphi_\infty(\Pi_s,\mathcal T_s)$ as $N\to\infty$ .

Degenerate cases.

$n=0$ : no initial state exists, so the statement is vacuous.
Real conventions: all quantities are finite and nonnegative, and all index sets are nonempty, so the conventions for empty or unbounded real suprema and infima do not arise.
$N=0$ : here $\varphi_0(\Pi,\mathcal T)=0$ , but $N=0$ is never required to satisfy the claim, since $N>N_\varepsilon\ge0$ .

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. (33), p. 786 — the finite-horizon robust value converges to the stationary game value ϕ∞(Πs,Ts)\phi_\infty(\Pi_s,\mathcal T_s)ϕ∞​(Πs​,Ts​)

Eq. (33), p. 786 — the finite-horizon robust value converges to the stationary game value $\phi_\infty(\Pi_s,\mathcal T_s)$