Step (c), p. 787 — against a stationary controller, stationary nature is as bad as time-varying nature

Proved

RobustMDP.Stationarity.stationaryPolicy_nature_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), for every stationary controller policy $\pi\in\Pi_s$ ,

\phi_\infty(\pi,\mathcal T):=\sup_{\tau\in\mathcal T}C_\infty(\pi,\tau)=\sup_{\tau\in\mathcal T_s}C_\infty(\pi,\tau)=:\phi_\infty(\pi,\mathcal T_s),

and consequently $\phi_\infty(\Pi_s,\mathcal T)=\phi_\infty(\Pi_s,\mathcal T_s)$ .

This is Step (c) of the proof of Theorem 4, the second 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 (c): for every stationary controller policy `π ∈ Π_s`,
the worst case over time-varying nature equals the worst case over stationary nature,
`φ_∞(π, 𝒯) = φ_∞(π, 𝒯_s)`; hence `φ_∞(Π_s, 𝒯) = φ_∞(Π_s, 𝒯_s)`. -/
theorem stationaryPolicy_nature_stationary {n : ℕ} {A : Type} [Fintype A] [Nonempty A]
    (M : Model n A) (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n) :
    (∀ π : Fin n → A,
      (⨆ τ : M.NaturePolicy, M.infCost ν i₀ (fun _ => π) τ) =
        ⨆ P : M.Choice, M.infCost ν i₀ (fun _ => π) (fun _ => P)) ∧
      M.phiInf_PsT ν 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 (c)

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 stationary controller is a single map $\sigma$ from states to actions, used at every time.
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$ . A stationary nature policy is a constant sequence $(P,P,\dots)$ .

The state distribution is $\mu_0=e_{i_0}$ , $\mu_{t+1}(j)=\sum_i\mu_t(i)P_t^{\sigma(i)}(i,j)$ . The infinite-horizon cost is

C_\infty(\sigma,\tau)=\sum_{t\ge0}\nu^t\sum_i\mu_t(i)\,c(i,\sigma(i)),

which is summable here.

Claim. Two things hold. All suprema and infima are real.

For every map $\sigma$ from states to actions:

\sup_{\tau}C_\infty(\sigma,\tau)=\sup_{P}C_\infty\big(\sigma,(P,P,\dots)\big).

$\varphi_\infty(\Pi_s,\mathcal T)=\varphi_\infty(\Pi_s,\mathcal T_s)$ , where

\varphi_\infty(\Pi_s,\mathcal T)=\inf_\sigma\sup_\tau C_\infty(\sigma,\tau),\qquad \varphi_\infty(\Pi_s,\mathcal T_s)=\inf_\sigma\sup_P C_\infty\big(\sigma,(P,P,\dots)\big).

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 do not arise.
$n=1$ : every transition is to the single state. Both sides of (1) then equal $c(0,\sigma(0))/(1-\nu)$ , so the claim is immediate.
Single-element sets: if every $\mathcal P_i^a$ has one element, time-varying and stationary nature policies coincide.

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