Discounted problems (Prop. 7.3.1)

Proved

BertsekasDP.discounted_main_theorem

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

bellmanequationdiscountedmdppolicyiteration

Proposition 7.3.1 (discounted problems). Consider the finite-state $\alpha$ -discounted problem, $0 < \alpha < 1$ , with stochastic transition rows $\sum_j p_{ij}(u) = 1$ at admissible controls. Then there is a cost vector $J^*$ for which all of the following hold:

Value iteration converges to $J^*$ from every initial vector;
Bellman's equation holds and determines $J^*$ uniquely:

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

$J^*$ is optimal: every admissible policy has a well-defined cost $\ge J^*$ , and some stationary policy attains it;
policy evaluation: each admissible stationary $\mu$ has a unique cost vector $J_\mu$ with $J_\mu = T_\mu^\alpha J_\mu$ , reached by value iteration under $\mu$ ;
optimality condition: $J_\mu = J^*$ if and only if $\mu$ attains the minimum in Bellman's equation at every state;
policy iteration generates an improving sequence of policies and terminates with an optimal one.

The discounted model is the workhorse of reinforcement learning, and its theory is entirely inherited: the source derives it by attaching to the discounted problem an associated stochastic shortest path problem in which the state terminates with probability $1 - \alpha$ at each stage, so that costs and value iterates coincide and Assumption 7.2.1 holds automatically.

Formalization Note The six parts are packaged as one statement so that they share the single existential witness $J^*$ , mirroring how the source states parts (a)–(e). Convergence is in the product topology on $\mathbb{R}^n$ , equivalently in any norm since $n$ is finite. Discounting appears only in the operators; the underlying model is the one of §7.2, with stochastic rows imposed as a hypothesis.

Preamble

import Mathlib
import Definitions.Def_BertsekasSSPModel

Formal statement

namespace BertsekasDP

theorem discounted_main_theorem {n : ℕ} {C : Type} [Fintype C]
    (M : BertsekasSSPModel n C) (α : ℝ) (hα : 0 < α ∧ α < 1)
    (hp1 : ∀ i, ∀ u ∈ M.U i, ∑ j, M.p i u j = 1) :
    ∃ Jstar : Fin n → ℝ,
      (∀ J₀ : Fin n → ℝ,
        Filter.Tendsto (fun k => (BertsekasDiscountedBellmanOp M α)^[k] J₀)
          Filter.atTop (nhds Jstar)) ∧
      BertsekasDiscountedBellmanOp M α Jstar = Jstar ∧
      (∀ J : Fin n → ℝ, BertsekasDiscountedBellmanOp M α J = J → J = Jstar) ∧
      (∀ π, BertsekasSSPAdmissible M π → ∀ i, ∃ Jπ : ℝ,
        Filter.Tendsto (fun N => BertsekasDiscountedNCost M α π N i)
          Filter.atTop (nhds Jπ) ∧ Jstar i ≤ Jπ) ∧
      (∃ μ : Fin n → C, (∀ i, μ i ∈ M.U i) ∧ ∀ i,
        Filter.Tendsto (fun N => BertsekasDiscountedNCost M α (fun _ => μ) N i)
          Filter.atTop (nhds (Jstar i))) ∧
      (∀ μ : Fin n → C, (∀ i, μ i ∈ M.U i) →
        ∃ Jμ : Fin n → ℝ,
          BertsekasDiscountedPolicyOp M α μ Jμ = Jμ ∧
          (∀ J : Fin n → ℝ,
            BertsekasDiscountedPolicyOp M α μ J = J → J = Jμ) ∧
          (∀ J₀ : Fin n → ℝ,
            Filter.Tendsto (fun k => (BertsekasDiscountedPolicyOp M α μ)^[k] J₀)
              Filter.atTop (nhds Jμ)) ∧
          (Jμ = Jstar ↔
            ∀ i, M.g i (μ i) + α * ∑ j, M.p i (μ i) j * Jstar j =
              BertsekasDiscountedBellmanOp M α Jstar i)) ∧
      (∀ (μ : ℕ → Fin n → C) (J : ℕ → Fin n → ℝ),
        (∀ k i, μ k i ∈ M.U i) →
        (∀ k, BertsekasDiscountedPolicyOp M α (μ k) (J k) = J k) →
        (∀ k i, M.g i (μ (k + 1) i) +
            α * ∑ j, M.p i (μ (k + 1) i) j * J k j =
          BertsekasDiscountedBellmanOp M α (J k) i) →
        (∀ k i, J (k + 1) i ≤ J k i) ∧
          ∃ k, BertsekasDiscountedBellmanOp 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.3.1

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$ , let $\alpha$ be a real number with $0 < \alpha$ and $\alpha < 1$ , and assume $hp1$ : for every state $i$ and every control $u \in U(i)$ , $\sum_j p_{ij}(u) = 1$ exactly (rows are genuinely stochastic on admissible controls; controls outside $U(i)$ remain unconstrained beyond nonnegativity). No survival/termination hypothesis is assumed. Write $T^\alpha$ for the discounted Bellman operator, $T^\alpha_\mu$ for the discounted policy operator, and $J^{\alpha,N}_\pi$ for the discounted $N$ -stage cost, all as defined in this bundle. The theorem asserts the existence of a function $J^* : \{0,\dots,n-1\} \to \mathbb{R}$ satisfying the conjunction of the following seven clauses:

Value iteration: for every $J_0$ , the iterates $(T^\alpha)^k J_0$ converge to $J^*$ as $k \to \infty$ (product/pointwise topology on $\mathbb{R}^{\{0,\dots,n-1\}}$ , equivalently uniform).
Fixed point: $T^\alpha J^* = J^*$ .
Uniqueness: every $J$ with $T^\alpha J = J$ equals $J^*$ .
Bound over admissible policy sequences, with convergence: for every policy sequence $\pi$ with $\pi_k(i) \in U(i)$ for all $k,i$ , and every state $i$ , there exists a real $J_\pi$ with $J^{\alpha,N}_\pi(i) \to J_\pi$ as $N \to \infty$ and $J^*(i) \le J_\pi$ . (Existence of the limit for every admissible $\pi$ is part of the claim.)
Attainment by a stationary policy: there exists $\mu : \{0,\dots,n-1\} \to C$ with $\mu(i) \in U(i)$ for all $i$ such that for every state $i$ , $J^{\alpha,N}_{(\mu,\mu,\dots)}(i) \to J^*(i)$ as $N \to \infty$ .
Policy evaluation and optimality condition for every stationary admissible $\mu$ : for every $\mu$ with $\mu(i) \in U(i)$ for all $i$ , there exists $J_\mu : \{0,\dots,n-1\} \to \mathbb{R}$ such that: (a) $T^\alpha_\mu J_\mu = J_\mu$ ; (b) every $J$ with $T^\alpha_\mu J = J$ equals $J_\mu$ ; (c) for every $J_0$ the iterates $(T^\alpha_\mu)^k J_0$ converge to $J_\mu$ ; and (d) the if and only if

J_\mu = J^* \iff \forall i,\ g(i,\mu(i)) + \alpha \sum_j p_{ij}(\mu(i))\, J^*(j) = (T^\alpha J^*)(i),

i.e. $J_\mu$ equals $J^*$ exactly when $\mu(i)$ attains the discounted Bellman minimum at $J^*$ for every state. 7. Policy iteration: for every sequence of stage policies $\mu_k$ with $\mu_k(i) \in U(i)$ for all $k,i$ , and every sequence of functions $J_k$ such that $T^\alpha_{\mu_k} J_k = J_k$ for every $k$ (each $J_k$ assumed to be a fixed point of its policy operator) and such that the improvement condition

\forall k, i:\quad g(i,\mu_{k+1}(i)) + \alpha \sum_j p_{ij}(\mu_{k+1}(i))\, J_k(j) = (T^\alpha J_k)(i)

holds, the conjunction follows: $J_{k+1}(i) \le J_k(i)$ for all $k, i$ , and there exists $k$ with $T^\alpha J_k = J_k$ .

The outer existence is $\exists$ , not $\exists!$ (clause 3 pins the fixed point down among fixed points). When $n = 0$ everything is vacuous or trivially witnessed. 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