One-step lookahead performance bound (Prop. 6.3.1)

Proved

BertsekasDP.one_step_lookahead_bound

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

lookaheadperformancebound

Proposition 6.3.1 (performance bound for one-step lookahead policies). In the basic stochastic model, let $\tilde J_k$ be cost-to-go approximations with $\tilde J_N = g_N$ , let $\bar U_k(x) \subseteq U_k(x)$ be restricted control sets, and let $\bar\pi$ be a one-step lookahead policy: $\bar\mu_k(x)$ attains

\hat J_k(x) \;=\; \min_{u \in \bar U_k(x)} \; \mathbb{E}_w\Bigl[g_k(x,u,w) + \tilde J_{k+1}\bigl(f_k(x,u,w)\bigr)\Bigr].

Assume the key condition (Eq. (6.20)) that this lookahead value never exceeds the approximation it is built from:

\hat J_k(x) \;\le\; \tilde J_k(x) \qquad \text{for all } x \text{ and } k < N .

Then the true cost-to-go $\bar J_k$ of the policy $\bar\pi$ satisfies

\bar J_k(x) \;\le\; \hat J_k(x) \;\le\; \tilde J_k(x) \qquad \text{for all } x \text{ and } k \le N .

Two things follow. First, the policy is at least as good as the approximation on which it is based — and via Example 6.3.1, taking $\tilde J$ to be the cost-to-go of a given heuristic policy shows that rolling out any policy improves it, the stochastic counterpart of Prop. 6.4.2. Second, $\hat J_k(x)$ , which is computed anyway when the control is selected, is a readily available upper bound on the policy's true performance.

Formalization Note The minimization defining the policy ranges over the restricted set $\bar U_k(x)$ only, as in Eq. (6.19); the sets are required nonempty implicitly, since the policy selects from them. The conclusion is proved by backward induction and is stated for all $k \le N$ , with the sharper first inequality asserted where $k < N$ .

Preamble

import Mathlib
import Definitions.Def_BertsekasDPModel

Formal statement

namespace BertsekasDP

theorem one_step_lookahead_bound {S C W : Type} [Fintype W]
    (M : BertsekasDPModel S C W)
    (Jt : ℕ → S → ℝ) (hJN : ∀ x, Jt M.N x = M.gN x)
    (Ubar : ℕ → S → Finset C)
    (hUsub : ∀ k x, Ubar k x ⊆ M.U k x)
    (π : ℕ → S → C)
    (hπmem : ∀ k x, π k x ∈ Ubar k x)
    (hπmin : ∀ k, k < M.N → ∀ x, ∀ u ∈ Ubar k x,
      ∑ w, M.p k x (π k x) w *
          (M.g k x (π k x) w + Jt (k + 1) (M.f k x (π k x) w)) ≤
        ∑ w, M.p k x u w * (M.g k x u w + Jt (k + 1) (M.f k x u w)))
    (h620 : ∀ k, k < M.N → ∀ x,
      ∑ w, M.p k x (π k x) w *
          (M.g k x (π k x) w + Jt (k + 1) (M.f k x (π k x) w)) ≤ Jt k x) :
    ∀ k, k ≤ M.N → ∀ x,
      (k < M.N →
        BertsekasDPPolicyCost M π (M.N - k) x ≤
          ∑ w, M.p k x (π k x) w *
            (M.g k x (π k x) w + Jt (k + 1) (M.f k x (π k x) w))) ∧
      BertsekasDPPolicyCost M π (M.N - k) x ≤ Jt k x := by sorry

end BertsekasDP

Source

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

Read-back

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

This statement is about types $S, C, W$ with $W$ finite and a term $M$ of the imported, not-provided structure BertsekasDPModel; only the fields used are visible: horizon $N = M.N \in \mathbb{N}$ , terminal cost $g_N : S \to \mathbb{R}$ , weights $p_k(x,u,w) \in \mathbb{R}$ , stage costs $g_k(x,u,w) \in \mathbb{R}$ , transitions $f_k(x,u,w) \in S$ , and constraint sets $U_k(x)$ , used here as finite sets of controls. It also refers to the imported, not-provided function BertsekasDPPolicyCost; write $J_\pi(m, x) \in \mathbb{R}$ for its value on the model $M$ , a policy $\pi$ , a step count $m \in \mathbb{N}$ , and a state $x$ — its definition is invisible to this audit, so the theorem is read with $J_\pi$ opaque. Hypotheses:

$J^\sim : \mathbb{N} \to S \to \mathbb{R}$ is any function ("lookahead approximation") with $J^\sim_N(x) = g_N(x)$ for all $x$ ;
$\bar U : \mathbb{N} \to S \to \operatorname{Finset} C$ satisfies $\bar U_k(x) \subseteq U_k(x)$ for all $k \in \mathbb{N}$ and all $x$ ;
$\pi : \mathbb{N} \to S \to C$ satisfies $\pi_k(x) \in \bar U_k(x)$ for all $k \in \mathbb{N}$ (including $k \ge N$ ) and all $x$ — so in particular every $\bar U_k(x)$ is forced nonempty, and hypotheses would be unsatisfiable if some $\bar U_k(x)$ were empty;
(hπmin) for every $k < N$ , every $x$ , and every $u \in \bar U_k(x)$ :

\sum_{w \in W} p_k(x, \pi_k(x), w)\big(g_k(x,\pi_k(x),w) + J^\sim_{k+1}(f_k(x,\pi_k(x),w))\big) \;\le\; \sum_{w \in W} p_k(x,u,w)\big(g_k(x,u,w) + J^\sim_{k+1}(f_k(x,u,w))\big),

i.e. $\pi_k(x)$ minimizes the one-step lookahead value (with cost-to-go $J^\sim_{k+1}$ ) over the restricted set $\bar U_k(x)$ — only over $\bar U$ , not over $U$ ;

(h620) for every $k < N$ and every $x$ , the same lookahead value of $\pi_k(x)$ is $\le J^\sim_k(x)$ .

The conclusion: for every $k \le N$ and every state $x$ , the conjunction of

if $k < N$ , then $J_\pi(N - k, x) \le \sum_{w} p_k(x, \pi_k(x), w)\big(g_k(x,\pi_k(x),w) + J^\sim_{k+1}(f_k(x,\pi_k(x),w))\big)$ , and
$J_\pi(N - k, x) \le J^\sim_k(x)$ ,

where $N - k$ is natural subtraction (harmless here since $k \le N$ ; at $k = N$ conjunct (1) is vacuous and (2) reads $J_\pi(0,x) \le J^\sim_N(x) = g_N(x)$ ). The proof is left as sorry.

Human review

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

View graph