Eq. (34), p. 786 — truncating the discounted cost at horizon $N$ loses at most $\nu^N c_{\max}/(1-\nu)$

Proved

RobustMDP.Stationarity.truncation_bound

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

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

Consider a robust discounted MDP with finite state space, finite nonempty action set, costs $c\ge0$ , nonempty row sets $\mathcal P_i^a\subseteq\Delta_n$ , and a discount factor $0<\nu<1$ . Let $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^N c_{\max}/(1-\nu)$ . Then for every controller policy $\pi\in\Pi$ , every nature policy $\tau\in\mathcal T$ and every horizon $N$ ,

C_N(\pi,\tau)\le C_\infty(\pi,\tau)\le C_N(\pi,\tau)+\varepsilon_N .

This elementary bound is used in every step of the proof of Theorem 4: it transfers statements about finite-horizon values to infinite-horizon ones with an error that vanishes at geometric rate $\nu$ .

Preamble

import Mathlib
import Definitions.Def_RobustMDP_Stationarity_Model

Formal statement

namespace RobustMDP.Stationarity

/-- Nilim–El Ghaoui 2005, p. 786, Eq. (34): for every `N`, every controller policy `π ∈ Π` and
every nature policy `τ ∈ 𝒯`, `C_N(π, τ) ≤ C_∞(π, τ) ≤ C_N(π, τ) + ε_N` with
`ε_N = ν^N c_max / (1 - ν)`. -/
theorem truncation_bound {n : ℕ} {A : Type} [Fintype A] [Nonempty A] (M : Model n A)
    (ν : ℝ) (hν₀ : 0 < ν) (hν₁ : ν < 1) (i₀ : Fin n)
    (π : Policy n A) (τ : M.NaturePolicy) (N : ℕ) :
    M.finiteCost ν i₀ N π τ ≤ M.infCost ν i₀ π τ ∧
      M.infCost ν i₀ π τ ≤ M.finiteCost ν 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. (34) (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 set of actions. The model $M$ gives:

a cost $c(i,a)\ge0$ for each state and action;
for each action $a$ and state $i$ , a nonempty set $\mathcal P_i^a$ of probability vectors on the states (entries $\ge0$ summing to 1). No convexity or closedness is assumed.

Let $\nu$ be a real number with $0<\nu<1$ , and let $i_0$ be an initial state.

A controller policy $\pi=(\pi_t)_{t\in\mathbb N}$ assigns an action $\pi_t(i)$ to each time $t$ and state $i$ .
A nature policy $\tau=(P_t)_{t\in\mathbb N}$ assigns to each time a family of matrices $(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},\qquad \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)),\qquad C_\infty(\pi,\tau)=\sum_{t\ge0}\nu^t\sum_i\mu_t(i)\,c(i,\pi_t(i)).

The infinite sum is taken as $0$ if not summable. Here the terms are nonnegative and at most $\nu^t c_{\max}$ , so the series is summable. The remaining constants are $c_{\max}=\max_{i,a}c(i,a)$ and $\varepsilon_N=\nu^N c_{\max}/(1-\nu)$ .

Claim. For every such $M$ , $\nu$ , $i_0$ , every controller policy $\pi$ , every nature policy $\tau$ and every $N\in\mathbb N$ :

C_N(\pi,\tau)\;\le\;C_\infty(\pi,\tau)\;\le\;C_N(\pi,\tau)+\varepsilon_N.

Degenerate cases.

$n=0$ : no initial state exists, so the statement is vacuous.
$n=1$ : every transition row is $(1)$ .
One action: there is exactly one controller policy.
$N=0$ : the claim reads $0\le C_\infty(\pi,\tau)\le c_{\max}/(1-\nu)$ .
Excluded values: $\nu=0$ and $\nu\ge1$ are excluded by hypothesis, so the division in $\varepsilon_N$ is by a positive number.

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. (34), p. 786 — truncating the discounted cost at horizon NNN loses at most νNcmax⁡/(1−ν)\nu^N c_{\max}/(1-\nu)νNcmax​/(1−ν)

Eq. (34), p. 786 — truncating the discounted cost at horizon $N$ loses at most $\nu^N c_{\max}/(1-\nu)$