SSP main theorem (Prop. 7.2.1(a),(b) + optimality)

Proved

BertsekasDP.ssp_main_theorem

by Shuze Chen · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

bellmanequationstochasticshortestpathvalueiteration

Proposition 7.2.1(a),(b) (the stochastic shortest path theorem). Consider the finite-state stochastic shortest path problem under Assumption 7.2.1: there is an integer $m > 0$ such that, regardless of the policy used and the initial state, termination is reached within $m$ stages with positive probability,

P\{x_m \ne t \mid x_0 = i, \pi\} \;<\; 1 \qquad \text{for every admissible } \pi \text{ and every state } i .

Then there is a cost vector $J^*$ such that:

Value iteration converges from every start: for any initial vector $J_0$ ,

\lim_{k \to \infty} (T^k J_0)(i) \;=\; J^*(i) \qquad \text{for every } i ;

$J^*$ satisfies Bellman's equation and is its unique solution:

J^*(i) \;=\; \min_{u \in U(i)} \Bigl[\, g(i,u) + \sum_{j=1}^{n} p_{ij}(u) J^*(j) \,\Bigr], \qquad i = 1,\dots,n ;

$J^*$ is the optimal cost: every admissible policy $\pi$ has a well-defined infinite-horizon cost $J_\pi(i) = \lim_N J^N_\pi(i)$ with $J^*(i) \le J_\pi(i)$ , and some admissible stationary policy attains $J^*$ .

This is the base case of infinite-horizon dynamic programming, and the theorem that value iteration and $Q$ -learning ultimately rest on: the Bellman operator has a unique fixed point which is the optimal cost, and it can be found by iterating from anywhere. The discounted theory of §7.3 is the special case where termination occurs with probability $1-\alpha$ at each stage.

Formalization Note Uniqueness of the fixed point is asserted over all real-valued cost vectors, with no boundedness side condition. The existence of the limit defining $J_\pi$ for nonstationary policies is part of the claim, not an assumption. Assumption 7.2.1 is stated through the survival probability under admissible policies; the source notes one may always take $m = n$ .

Preamble

import Mathlib
import Definitions.Def_BertsekasSSPModel

Formal statement

namespace BertsekasDP

theorem ssp_main_theorem {n : ℕ} {C : Type} [Fintype C]
    (M : BertsekasSSPModel n C)
    (hA : ∃ m : ℕ, 0 < m ∧ ∀ π, BertsekasSSPAdmissible M π →
      ∀ i, BertsekasSSPSurvival M π m i < 1) :
    ∃ Jstar : Fin n → ℝ,
      (∀ J₀ : Fin n → ℝ,
        Filter.Tendsto (fun k => (BertsekasSSPBellmanOp M)^[k] J₀)
          Filter.atTop (nhds Jstar)) ∧
      BertsekasSSPBellmanOp M Jstar = Jstar ∧
      (∀ J : Fin n → ℝ, BertsekasSSPBellmanOp M J = J → J = Jstar) ∧
      (∀ π, BertsekasSSPAdmissible M π → ∀ i, ∃ Jπ : ℝ,
        Filter.Tendsto (fun N => BertsekasSSPNCost M π N i)
          Filter.atTop (nhds Jπ) ∧ Jstar i ≤ Jπ) ∧
      (∃ μ : Fin n → C, (∀ i, μ i ∈ M.U i) ∧ ∀ i,
        Filter.Tendsto (fun N => BertsekasSSPNCost M (fun _ => μ) N i)
          Filter.atTop (nhds (Jstar i))) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 7.2.1(a),(b)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $n \in \mathbb{N}$ , $C$ a finite type, and $M$ a BertsekasSSPModel on $n$ states with controls in $C$ (so the transition rows satisfy $p_{ij}(u)\ge 0$ for all $u$ and $\sum_j p_{ij}(u) \le 1$ for $u \in U(i)$ ; there is no requirement that the rows sum to exactly $1$ ). Assume the hypothesis $hA$ : there exists $m \in \mathbb{N}$ with $m > 0$ such that for every policy sequence $\pi$ satisfying the admissibility condition $\pi_k(i) \in U(i)$ for all $k,i$ , and for every state $i$ ,

S^m_\pi(i) < 1,

where $S^m_\pi(i)$ is the $m$ -step survival mass defined above (the probability of remaining in the state space for $m$ steps under $\pi$ ). The theorem then asserts the existence of a function $J^* : \{0,\dots,n-1\} \to \mathbb{R}$ (existence only, $\exists$ , not $\exists!$ ) satisfying the conjunction of the following five clauses, where $T$ is the SSP Bellman operator and $J^N_\pi$ the $N$ -stage cost defined above:

Value iteration converges from every start: for every $J_0 : \{0,\dots,n-1\} \to \mathbb{R}$ , the sequence of $k$ -fold iterates $T^k J_0$ converges to $J^*$ as $k \to \infty$ , in the topology of the finite product space $\mathbb{R}^{\{0,\dots,n-1\}}$ (pointwise convergence, which for finite $n$ coincides with uniform convergence).
Fixed point: $T J^* = J^*$ (equality of functions).
Uniqueness of the fixed point: every $J$ with $T J = J$ equals $J^*$ — quantified over all real-valued functions $J$ on the states, with no boundedness or other side condition.
Lower bound over admissible policies, with convergence: for every policy sequence $\pi$ that is admissible ( $\pi_k(i) \in U(i)$ for all $k,i$ ), and every state $i$ , there exists a real number $J_\pi$ such that $J^N_\pi(i) \to J_\pi$ as $N \to \infty$ and $J^*(i) \le J_\pi$ . Note this clause asserts, for each admissible $\pi$ and each $i$ , the existence of the limit of the $N$ -stage costs, not merely a bound.
A stationary policy attains $J^*$ : there exists a single stage policy $\mu : \{0,\dots,n-1\} \to C$ with $\mu(i) \in U(i)$ for all $i$ , such that for every state $i$ the $N$ -stage cost of the constant policy sequence $(\mu,\mu,\dots)$ converges to $J^*(i)$ as $N \to \infty$ .

If $n = 0$ the state space is empty, hypothesis $hA$ is satisfiable (e.g. $m=1$ vacuously), and all clauses are vacuous or trivially witnessed. The theorem's proof is not supplied in this file (the body is a placeholder).

Human review

Endorsed by Community (Bot) · Sep 8, 2026
Endorsed by Shuze Chen · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph