Step (d), p. 787 — nominal stationarity (Puterman 1994): $\phi_N(\Pi,\tau)\to\phi_\infty(\Pi_s,\tau)$ for stationary $\tau$

Proved

RobustMDP.Stationarity.nominal_stationarity

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

dynamic-programmingmarkov-decision-processp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix 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) and a stationary nature policy $\tau\in\mathcal T_s$ , that is, fixed transition matrices $(P^a)_{a}$ with rows $P^a(i,\cdot)\in\mathcal P_i^a$ used at every stage. Then the nominal finite-horizon optimal values converge to the nominal infinite-horizon optimal value over stationary policies:

\phi_N(\Pi,\tau):=\inf_{\pi\in\Pi}C_N(\pi,\tau)\ \xrightarrow[N\to\infty]{}\ \phi_\infty(\Pi_s,\tau):=\inf_{\pi\in\Pi_s}C_\infty(\pi,\tau).

The paper imports this from the classical theory of discounted MDPs (Puterman 1994) and uses it in Step (d) of the proof of Theorem 4.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Stationarity_Model

Formal statement

namespace RobustMDP.Stationarity

/-- Nilim–El Ghaoui 2005, p. 787, Step (d), the nominal fact cited to Puterman (1994): for every
stationary nature policy `τ = (P, P, …) ∈ 𝒯_s`, `φ_N(Π, τ) = inf_{π ∈ Π} C_N(π, τ)` converges,
as `N → ∞`, to `φ_∞(Π_s, τ) = inf_{π ∈ Π_s} C_∞(π, τ)`. -/
theorem nominal_stationarity {n : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n A) (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) (P : M.Choice) :
    Filter.Tendsto (fun N : ℕ => ⨅ π : Policy n A, M.finiteCost ν i₀ N π (fun _ => P))
      Filter.atTop
      (nhds (⨅ π : Fin n → A, M.infCost ν i₀ (fun _ => π) (fun _ => P))) := 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 (d), citing Puterman (1994)

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.

Let $0<\nu<1$ and let $i_0$ be an initial state. Fix one choice of nature $P=(P^a)_{a\in A}$ , a family of $n\times n$ matrices with rows $P^a(i,\cdot)\in\mathcal P_i^a$ . It is used at every time step.

A controller policy $\pi=(\pi_t)_{t\in\mathbb N}$ is a sequence of maps from states to actions.
A stationary controller is a single map $\sigma$ used at every time.

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)=\sum_{t=0}^{N-1}\nu^t\sum_i\mu_t(i)c(i,\pi_t(i)),

and $C_\infty(\sigma)=\sum_{t\ge0}\nu^t\sum_i\mu_t(i)c(i,\sigma(i))$ for stationary $\sigma$ , which is summable here.

Claim. As $N\to\infty$ ,

\inf_{\pi}C_N(\pi)\;\longrightarrow\;\inf_{\sigma}C_\infty(\sigma).

The left infimum is over all (possibly time-varying) controller policies. The right infimum is over all maps $\sigma$ from states to actions, used stationarily. The only uncertainty-related input is the fixed $P$ ; the sets $\mathcal P_i^a$ matter only in that $P$ 's rows lie in them.

Degenerate cases.

$n=0$ : no initial state exists, so the statement is vacuous.
$N=0$ : the left-hand side is $0$ , which does not affect a limit statement.
Real conventions: all costs are nonnegative and bounded, and all index sets are nonempty, so the conventions for empty or unbounded-below real infima do not arise.
One action: both sides involve a single policy, and the claim reduces to $C_N\to C_\infty$ for that policy.

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 (d), p. 787 — nominal stationarity (Puterman 1994): ϕN(Π,τ)→ϕ∞(Πs,τ)\phi_N(\Pi,\tau)\to\phi_\infty(\Pi_s,\tau)ϕN​(Π,τ)→ϕ∞​(Πs​,τ) for stationary τ\tauτ

Step (d), p. 787 — nominal stationarity (Puterman 1994): $\phi_N(\Pi,\tau)\to\phi_\infty(\Pi_s,\tau)$ for stationary $\tau$