Eq. (5.5) — the approximations in policy space decrease monotonically

Proved

BellmanRouting.PolicySpace.approx_succ_le

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programmingp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1shortest-pathsuccessive-approximations

Let $N = n + 1 \ge 2$ and $t_{ij} > 0$ for $i \ne j$ , and let $f^{(k)}$ be defined by (5.1) from the direct-route policy (5.2), with $f_N^{(0)} = 0$ . Then

f_i^{(k+1)} \le f_i^{(k)}, \qquad i = 1, 2, \dots, N, \quad k = 0, 1, 2, \dots

The monotone decrease is the "approximation in policy space" property: each iterate is the value of a policy no worse than the previous one.

Formalization Note $f_N^{(0)} = 0$ is the corrected reading of (5.2); see the (5.4) item. With the printed $f_N^{(0)} = t_{NN} > 0$ the inequality fails already at $k = 0$ .

Preamble

import Mathlib
import Definitions.Def_BellmanRouting_PolicySpace_Routing

Formal statement

namespace BellmanRouting.PolicySpace

theorem approx_succ_le {n : ℕ} (hn : 1 ≤ n)
    (t : Fin (n + 1) → Fin (n + 1) → ℝ) (ht : ∀ i j, i ≠ j → 0 < t i j) :
    ∀ k i, approx t (k + 1) i ≤ approx t k i := by sorry

end BellmanRouting.PolicySpace

Source

Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), p. 89, Section 5, Eq. (5.5)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph