Policy evaluation (Prop. 7.2.1(c))

Proved

BertsekasDP.ssp_policy_evaluation

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

policyevaluation

Proposition 7.2.1(c) (policy evaluation). Under Assumption 7.2.1, let $\mu$ be any admissible stationary policy. Then its cost vector $J_\mu$ is the unique solution of the linear system

J_\mu(i) \;=\; g\bigl(i, \mu(i)\bigr) \;+\; \sum_{j=1}^{n} p_{ij}\bigl(\mu(i)\bigr) J_\mu(j), \qquad i = 1, \dots, n,

the iteration $J_{k+1} = T_\mu J_k$ converges to $J_\mu$ from every initial vector, and $J_\mu$ is the limit of the $N$ -stage costs of $\mu$ :

\lim_{k \to \infty} (T_\mu^k J_0)(i) \;=\; J_\mu(i) \;=\; \lim_{N \to \infty} J^N_{\mu}(i) \qquad \text{for every } i .

This is the single-policy case of the main theorem, and the computational workhorse of policy iteration: evaluating a policy is solving one linear system of $n$ equations, or equivalently iterating a contraction. That the same vector is both the fixed point and the limit of finite-horizon costs is what makes the two views of "the cost of $\mu$ " interchangeable.

Formalization Note Uniqueness is asserted among all real-valued vectors. Under Assumption 7.2.1 the operator $T_\mu$ is a contraction after $m$ stages rather than after one, which is where the finiteness of the policy space enters the proof.

Preamble

import Mathlib
import Definitions.Def_BertsekasSSPModel

Formal statement

namespace BertsekasDP

theorem ssp_policy_evaluation {n : ℕ} {C : Type} [Fintype C]
    (M : BertsekasSSPModel n C)
    (hA : ∃ m : ℕ, 0 < m ∧ ∀ π, BertsekasSSPAdmissible M π →
      ∀ i, BertsekasSSPSurvival M π m i < 1)
    (μ : Fin n → C) (hμ : ∀ i, μ i ∈ M.U i) :
    ∃ Jμ : Fin n → ℝ,
      BertsekasSSPPolicyOp M μ Jμ = Jμ ∧
      (∀ J : Fin n → ℝ, BertsekasSSPPolicyOp M μ J = J → J = Jμ) ∧
      (∀ J₀ : Fin n → ℝ,
        Filter.Tendsto (fun k => (BertsekasSSPPolicyOp M μ)^[k] J₀)
          Filter.atTop (nhds Jμ)) ∧
      (∀ i, Filter.Tendsto (fun N => BertsekasSSPNCost M (fun _ => μ) N i)
        Filter.atTop (nhds (Jμ 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(c)

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 the same hypothesis $hA$ as in ssp_main_theorem: there is an $m > 0$ such that every admissible policy sequence $\pi$ (meaning $\pi_k(i) \in U(i)$ for all $k,i$ ) has $m$ -step survival mass $S^m_\pi(i) < 1$ at every state $i$ . Let $\mu : \{0,\dots,n-1\} \to C$ be a stage policy with $\mu(i) \in U(i)$ for every $i$ . The theorem asserts the existence of a function $J_\mu : \{0,\dots,n-1\} \to \mathbb{R}$ such that all four of the following hold, where $T_\mu$ is the policy operator $(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j)$ :

$T_\mu J_\mu = J_\mu$ (as functions);
every $J : \{0,\dots,n-1\} \to \mathbb{R}$ with $T_\mu J = J$ equals $J_\mu$ (uniqueness of the fixed point among all real-valued functions);
for every starting function $J_0$ , the iterates $T_\mu^k J_0$ converge to $J_\mu$ as $k \to \infty$ (in the product/pointwise topology on $\mathbb{R}^{\{0,\dots,n-1\}}$ , equivalently uniform since $n$ is finite);
for every state $i$ , the $N$ -stage cost $J^N_{(\mu,\mu,\dots)}(i)$ of the constant policy sequence converges to $J_\mu(i)$ as $N \to \infty$ .

No connection between $J_\mu$ and any optimal value function is asserted. 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