Policy iteration (Prop. 7.2.2)

Proved

BertsekasDP.ssp_policy_iteration

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

policyiteration

Proposition 7.2.2 (policy iteration). Under Assumption 7.2.1, consider policy iteration: starting from an admissible stationary policy $\mu^0$ , alternately evaluate the current policy, solving $J_k = T_{\mu^k} J_k$ , and improve it, choosing $\mu^{k+1}(i)$ to attain

\min_{u \in U(i)} \Bigl[\, g(i,u) + \sum_{j=1}^{n} p_{ij}(u) J_k(j) \,\Bigr] \qquad \text{for every } i .

Then the generated policies improve monotonically and the algorithm terminates with an optimal policy:

J_{k+1}(i) \;\le\; J_k(i) \quad \text{for all } i \text{ and } k, \qquad\text{and}\qquad J_k = T J_k \ \text{ for some } k .

Policy iteration is the alternative to value iteration that terminates finitely rather than in the limit: each iteration either strictly improves some state's cost or has already reached a solution of Bellman's equation, and there are only finitely many stationary policies. In practice it converges in very few iterations, at the price of solving a linear system per step.

Formalization Note The evaluations $J_k$ are given as fixed points of the corresponding policy operators, matching the linear system solved in practice. Reaching a $k$ with $T J_k = J_k$ is exactly optimality by Prop. 7.2.1(b),(d).

Preamble

import Mathlib
import Definitions.Def_BertsekasSSPModel

Formal statement

namespace BertsekasDP

theorem ssp_policy_iteration {n : ℕ} {C : Type} [Fintype C]
    (M : BertsekasSSPModel n C)
    (hA : ∃ m : ℕ, 0 < m ∧ ∀ π, BertsekasSSPAdmissible M π →
      ∀ i, BertsekasSSPSurvival M π m i < 1)
    (μ : ℕ → Fin n → C) (hadm : ∀ k i, μ k i ∈ M.U i)
    (J : ℕ → Fin n → ℝ)
    (heval : ∀ k, BertsekasSSPPolicyOp M (μ k) (J k) = J k)
    (himp : ∀ k i,
      M.g i (μ (k + 1) i) + ∑ j, M.p i (μ (k + 1) i) j * J k j =
        BertsekasSSPBellmanOp M (J k) i) :
    (∀ k i, J (k + 1) i ≤ J k i) ∧
    (∃ k, BertsekasSSPBellmanOp M (J k) = J k) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 7.2.2

Read-back

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

Let $M$ be a BertsekasSSPModel on $n$ states with finite control type $C$ , and assume $hA$ : there is an $m > 0$ such that every admissible policy sequence has $m$ -step survival mass strictly less than $1$ at every state. Suppose given:

a sequence of stage policies $\mu_k : \{0,\dots,n-1\} \to C$ ( $k \in \mathbb{N}$ ) with $\mu_k(i) \in U(i)$ for all $k, i$ ;
a sequence of functions $J_k : \{0,\dots,n-1\} \to \mathbb{R}$ such that for every $k$ , $T_{\mu_k} J_k = J_k$ — each $J_k$ is assumed to be a fixed point of the corresponding policy operator (nothing here forces it to be the unique one, though the given functions are the ones the conclusions speak about);
the policy improvement hypothesis: for every $k$ and every state $i$ ,

g(i, \mu_{k+1}(i)) + \sum_j p_{ij}(\mu_{k+1}(i))\, J_k(j) = (T J_k)(i),

i.e. the control $\mu_{k+1}(i)$ exactly attains the Bellman minimum for $J_k$ at every state.

The conclusion is the conjunction of two claims:

Monotonicity: for every $k$ and every state $i$ , $J_{k+1}(i) \le J_k(i)$ (non-strict, pointwise).
Finite arrival at a Bellman fixed point: there exists a $k$ such that $T J_k = J_k$ (equality of functions).

Nothing is asserted about $J_k$ equaling any optimal value, about the policies stabilizing, or about what happens after such a $k$ . The proof 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