Step (d), p. 787 — $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$

Proved

RobustMDP.Stationarity.stationaryNature_policy_stationary

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), when nature is restricted to stationary policies, allowing the controller time-varying policies does not lower the robust value:

\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s).

This is Step (d) of the proof of Theorem 4, the last equality of (31).

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 (d): `φ_∞(Π, 𝒯_s) = φ_∞(Π_s, 𝒯_s)`. -/
theorem stationaryNature_policy_stationary {n : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n A) (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) :
    M.phiInf_PTs ν i₀ = 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. 787, proof of Theorem 4, Step (d), 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 stationary one is a single map $\sigma$ used at every time.
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.

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 infinite-horizon cost is

C_\infty(\pi,P)=\sum_{t\ge0}\nu^t\sum_i\mu_t(i)c(i,\pi_t(i)),

which is summable here.

Claim.

\inf_{\pi}\sup_{P}C_\infty(\pi,P)\;=\;\inf_{\sigma}\sup_{P}C_\infty(\sigma,P).

The left infimum is over all (possibly time-varying) controller policies. The right infimum is over single maps $\sigma$ used at every time. Both suprema are over single choices of nature held constant through time, and all suprema and infima are real.

Degenerate cases.

$n=0$ : no initial state exists, so the statement is vacuous.
Real conventions: all quantities lie in $[0,c_{\max}/(1-\nu)]$ with $c_{\max}=\max c$ , and all index sets are nonempty, so the conventions for empty or unbounded real suprema and infima do not arise.
One action: both sides range over the same single policy and are trivially equal.
$n=1$ : both sides equal $\min_a c(0,a)/(1-\nu)$ .

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 — ϕ∞(Π,Ts)=ϕ∞(Πs,Ts)\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)ϕ∞​(Π,Ts​)=ϕ∞​(Πs​,Ts​)

Step (d), p. 787 — $\phi_\infty(\Pi,\mathcal T_s)=\phi_\infty(\Pi_s,\mathcal T_s)$