Eq. (35), p. 786 — $\phi_N(\Pi,\mathcal T)\to\phi_\infty(\Pi,\mathcal T)$ at geometric rate $\nu$

Proved

RobustMDP.Stationarity.timeVarying_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)\le\phi_\infty(\Pi,\mathcal T)\le\phi_N(\Pi,\mathcal T)+\varepsilon_N,\qquad \varepsilon_N=\frac{\nu^N c_{\max}}{1-\nu},

where $\phi_N(\Pi,\mathcal T)=\inf_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)$ is the finite-horizon robust value under time-varying uncertainty and $\phi_\infty(\Pi,\mathcal T)$ its infinite-horizon counterpart.

Hence the finite-horizon robust values converge to the infinite-horizon one geometrically at rate $\nu$ (Step (b) of the proof of 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. 786, Step (b), Eq. (35): for every `N`,
`φ_N(Π, 𝒯) ≤ φ_∞(Π, 𝒯) ≤ φ_N(Π, 𝒯) + ε_N`. -/
theorem timeVarying_value_converges {n : ℕ} {A : Type} [Fintype A] [Nonempty A] (M : Model n A)
    (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) (N : ℕ) :
    M.phiN_PT ν i₀ N ≤ M.phiInf_PT ν i₀ ∧
      M.phiInf_PT ν i₀ ≤ M.phiN_PT ν 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. 786, Eq. (35) (proof of Theorem 4, Step (b))

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(\pi,\tau)$ is the corresponding infinite sum. It is summable here, since its terms are nonnegative and at most $\nu^tc_{\max}$ .

The two values compared are

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

Both infima range over all controller policies and both suprema over all nature policies, taken as real infima and suprema. Finally $\varepsilon_N=\nu^N c_{\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: under the hypotheses, all costs lie in $[0,c_{\max}/(1-\nu)]$ and all index sets are nonempty. So the convention that makes empty or unbounded real suprema and infima equal to $0$ does not come into play.
One action: there is only one controller policy, and the infimum 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

Eq. (35), p. 786 — ϕN(Π,T)→ϕ∞(Π,T)\phi_N(\Pi,\mathcal T)\to\phi_\infty(\Pi,\mathcal T)ϕN​(Π,T)→ϕ∞​(Π,T) at geometric rate ν\nuν

Eq. (35), p. 786 — $\phi_N(\Pi,\mathcal T)\to\phi_\infty(\Pi,\mathcal T)$ at geometric rate $\nu$