General lookahead bound with slacks (Prop. 6.3.2)

Proved

BertsekasDP.limited_lookahead_bound

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

lookaheadperformancebound

Proposition 6.3.2 (performance bound with per-stage slacks). In the basic stochastic model, let $\tilde J_k$ be arbitrary functions with $\tilde J_N = g_N$ , and let $\bar\pi$ be an admissible policy which at every stage falls short of the approximation by at most $\delta_k$ (Eq. (6.23)):

\mathbb{E}_w\Bigl[g_k\bigl(x,\bar\mu_k(x),w\bigr) + \tilde J_{k+1}\bigl(f_k(x,\bar\mu_k(x),w)\bigr)\Bigr] \;\le\; \tilde J_k(x) + \delta_k \qquad \text{for all } x, \; k < N .

Then the cost-to-go of $\bar\pi$ obeys the accumulated bound

J_{\bar\pi,k}(x) \;\le\; \tilde J_k(x) \;+\; \sum_{i=k}^{N-1} \delta_i \qquad \text{for all } x \text{ and } k \le N .

Unlike Prop. 6.3.1 this needs no assumption relating $\tilde J$ to a minimization, which makes it the tool of choice when the lookahead minimization is inexact, when the approximation architecture is imperfect, or when the policy comes from elsewhere entirely. The source uses it to bound the certainty equivalent controller, where $\delta_k$ measures the error committed by fixing the disturbance at a nominal value; when every $\delta_k \le 0$ it recovers $J_{\bar\pi,k} \le \tilde J_k$ .

Formalization Note The scalars $\delta_k$ carry no sign restriction. No minimality of $\bar\pi$ over any control set is hypothesized — only the displayed inequality — though the policy is required to be admissible. The sum over the empty range at $k = N$ gives the boundary case $J_{\bar\pi,N} \le g_N$ .

Preamble

import Mathlib
import Definitions.Def_BertsekasDPModel

Formal statement

namespace BertsekasDP

theorem limited_lookahead_bound {S C W : Type} [Fintype W]
    (M : BertsekasDPModel S C W)
    (Jt : ℕ → S → ℝ) (hJN : ∀ x, Jt M.N x = M.gN x)
    (δ : ℕ → ℝ)
    (π : ℕ → S → C)
    (hadm : ∀ k x, π k x ∈ M.U k x)
    (hπ : ∀ 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, k ≤ M.N → ∀ x,
      BertsekasDPPolicyCost M π (M.N - k) x ≤
        Jt k x + ∑ i ∈ Finset.Ico k M.N, δ i := by sorry

end BertsekasDP

Source

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

Read-back

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

Same setting: types $S, C, W$ with $W$ finite, $M$ a term of the not-provided structure BertsekasDPModel (visible fields as above: $N$ , $g_N$ , $p_k$ , $g_k$ , $f_k$ , $U_k$ ), and the not-provided quantity $J_\pi(m,x) =$ BertsekasDPPolicyCost treated as opaque. Hypotheses:

$J^\sim : \mathbb{N} \to S \to \mathbb{R}$ with $J^\sim_N(x) = g_N(x)$ for all $x$ ;
$\delta : \mathbb{N} \to \mathbb{R}$ is an arbitrary real sequence (no sign constraint);
$\pi : \mathbb{N} \to S \to C$ with $\pi_k(x) \in U_k(x)$ for all $k \in \mathbb{N}$ and all $x$ (again forcing every $U_k(x)$ nonempty for the hypotheses to be satisfiable);
(hπ) for every $k < N$ and every $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\; J^\sim_k(x) + \delta_k,

i.e. the policy's one-step lookahead value with cost-to-go $J^\sim_{k+1}$ exceeds $J^\sim_k(x)$ by at most $\delta_k$ . (No minimality of $\pi$ over any control set is hypothesized — only this inequality.)

Conclusion: for every $k \le N$ and every state $x$ ,

J_\pi(N - k,\, x) \;\le\; J^\sim_k(x) + \sum_{i = k}^{N-1} \delta_i,

where $N - k$ is natural subtraction (no truncation occurs since $k \le N$ ) and the sum runs over the integer interval $\{k, k+1, \dots, N-1\}$ , which is empty when $k = N$ (giving $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