HJB sufficiency theorem (Prop. 3.2.1)

Disproved

BertsekasDP.hjb_sufficiency

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

hjbequationverificationtheorem

Proposition 3.2.1 (Sufficiency Theorem for the HJB equation). Suppose $V(t,x)$ is continuously differentiable and solves the Hamilton–Jacobi–Bellman equation: for every $t \in [0,T]$ and every state $x$ ,

0 \;=\; \min_{u \in U} \Bigl[\, g(x,u) \;+\; \partial_t V(t,x) \;+\; \bigl\langle \nabla_x V(t,x), \, f(x,u) \bigr\rangle \,\Bigr],

with the boundary condition $V(T,x) = h(x)$ . Then:

$V$ is a lower bound on the cost-to-go. For every start $(t_0,\xi)$ with $t_0 \in [0,T]$ and every admissible control/state pair $(u,x)$ on $[t_0,T]$ with $x(t_0) = \xi$ ,

V(t_0,\xi) \;\le\; h\bigl(x(T)\bigr) + \int_{t_0}^{T} g\bigl(x(t),u(t)\bigr)\,dt .

A trajectory attaining the minimum is optimal. If an admissible pair $(u^*,x^*)$ from $(t_0,\xi)$ satisfies the HJB expression with equality at every time — that is, $u^*(t)$ attains the minimum above along $x^*(t)$ — then its cost equals $V(t_0,\xi)$ exactly.

Together the two parts say that a classical solution of the HJB equation is the optimal cost-to-go function and that greedy minimization against it yields an optimal control. This is the verification direction of dynamic programming in continuous time: hard to apply when $V$ is unknown, decisive when a candidate $V$ can be guessed, as for the linear-quadratic problem.

Formalization Note The HJB condition is stated as " $0$ is the greatest lower bound" of the bracketed set over $u \in U$ , so the minimum need not be attained; if $U$ is empty the hypothesis is unsatisfiable and the theorem is vacuous. The statement is about a given $V$ : it does not assert that such a $V$ exists, nor that an optimal control exists. Part 2 requires the equality at every time of the interval, with no exceptional set.

Retired — this statement is false as written. It carried no regularity hypothesis on the system function $f$ or the running cost $g$ , although the standing assumptions of Chapter 3 (§3.1 of the source) make them continuously differentiable in $x$ and continuous in $u$ . Without regularity the cost integrand $t \mapsto g(x(t),u(t))$ need not be integrable, and the interval integral then takes the library's junk value $0$ ; the accepted disproof (PupAtlas) takes $g(x,u) = 1 + |u|/|x|$ , $f(x,u) = u$ , $V(t,x) = -t$ , $h = -1$ , so the HJB hypothesis holds while the trajectory $x(t) = t - \tfrac12$ under $u \equiv 1$ has a non-integrable cost and the claimed inequality $V(0,\xi) \le \mathrm{cost}$ reads $0 \le -1$ .

It is replaced by BertsekasDP.hjb_sufficiency_of_continuous, which assumes $f$ and $g$ jointly continuous — the consequence of the source's standing assumptions that the sufficiency proof uses — and is otherwise identical. The omission was mine as the mission's captain.

Preamble

import Mathlib
import Definitions.Def_BertsekasCTModel

Formal statement

namespace BertsekasDP

open scoped RealInnerProductSpace

theorem hjb_sufficiency {n m : ℕ} (M : BertsekasCTModel n m)
    (V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ)
    (hV : ContDiff ℝ 1 (Function.uncurry V))
    (hHJB : ∀ t ∈ Set.Icc 0 M.T, ∀ x : EuclideanSpace ℝ (Fin n),
      IsGLB ((fun u => M.g x u + deriv (fun s => V s x) t +
        ⟪gradient (V t) x, M.f x u⟫) '' M.U) 0)
    (hbdry : ∀ x, V M.T x = M.h x) :
    (∀ t₀ ∈ Set.Icc 0 M.T, ∀ ξ u x,
      BertsekasCTAdmissibleFrom M t₀ ξ u x →
        V t₀ ξ ≤ BertsekasCTCostFrom M t₀ u x) ∧
    (∀ t₀ ∈ Set.Icc 0 M.T, ∀ ξ ustar xstar,
      BertsekasCTAdmissibleFrom M t₀ ξ ustar xstar →
      (∀ t ∈ Set.Icc t₀ M.T,
        M.g (xstar t) (ustar t) + deriv (fun s => V s (xstar t)) t +
          ⟪gradient (V t) (xstar t), M.f (xstar t) (ustar t)⟫ = 0) →
        BertsekasCTCostFrom M t₀ ustar xstar = V t₀ ξ) := by sorry

end BertsekasDP

Source

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

Read-back

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

Fix $n, m \in \mathbb{N}$ (implicit) and a model $M = (T, U, f, g, h, x_0)$ of type $\mathrm{BertsekasCTModel}\ n\ m$ (so $T > 0$ ; $f, g, h$ carry no regularity from the structure, and the field $x_0$ plays no role in this statement). Given:

$V : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}$ , assumed jointly $C^1$ in $(t, x)$ on all of $\mathbb{R} \times \mathbb{R}^n$ ;
HJB hypothesis: for every $t \in [0, T]$ and every $x \in \mathbb{R}^n$ (all of space, not just reachable states), the number $0$ is the greatest lower bound (infimum, not necessarily attained) of the set

\Big\{\, g(x, u) + \tfrac{\partial}{\partial s} V(s, x)\big|_{s=t} + \big\langle \nabla_x V(t, x),\, f(x, u) \big\rangle \;:\; u \in U \,\Big\} \subseteq \mathbb{R},

where $\tfrac{\partial}{\partial s}V(s,x)|_{s=t}$ is the one-variable derivative in time (space frozen at $x$ ) and $\nabla_x V(t, x)$ is the spatial gradient (time frozen at $t$ ). "Greatest lower bound" means both: every element of the set is $\ge 0$ , and every lower bound of the set is $\le 0$ . Edge case: if $U = \varnothing$ the set is empty, and $0$ cannot be its greatest lower bound (every real is a lower bound of $\varnothing$ ), so this hypothesis forces $U \neq \varnothing$ ;

boundary hypothesis: $V(T, x) = h(x)$ for every $x \in \mathbb{R}^n$ .

Conclusion — the conjunction of two claims.

(a) Lower-bound claim. For every $t_0 \in [0, T]$ , every $\xi \in \mathbb{R}^n$ , and every pair $(u, x)$ of functions $u : \mathbb{R} \to \mathbb{R}^m$ , $x : \mathbb{R} \to \mathbb{R}^n$ that is admissible from $(t_0, \xi)$ in this bundle's sense — i.e. $u(t) \in U$ on $[t_0, T]$ ; $u$ bounded on $[t_0, T]$ and continuous there off some finite set; $x$ continuous on $[t_0, T]$ with $x(t_0) = \xi$ ; and $x' (t) = f(x(t), u(t))$ (two-sided derivative) for all $t \in [t_0, T]$ off some finite set — one has

V(t_0, \xi) \;\le\; h(x(T)) + \int_{t_0}^{T} g(x(t), u(t))\, dt,

the right side being this bundle's cost $\mathrm{BertsekasCTCostFrom}(M, t_0, u, x)$ (recall the interval integral evaluates to $0$ if the integrand is not integrable).

(b) Attainment claim. For every $t_0 \in [0, T]$ , every $\xi \in \mathbb{R}^n$ , and every admissible-from- $(t_0, \xi)$ pair $(u^*, x^*)$ that additionally satisfies, for every $t \in [t_0, T]$ (every point of the closed interval, exceptional points of the trajectory included),

g(x^*(t), u^*(t)) + \tfrac{\partial}{\partial s} V(s, x^*(t))\big|_{s=t} + \big\langle \nabla_x V(t, x^*(t)),\, f(x^*(t), u^*(t)) \big\rangle = 0,

one has the exact equality

h(x^*(T)) + \int_{t_0}^{T} g(x^*(t), u^*(t))\, dt \;=\; V(t_0, \xi).

No claim of existence of an optimal control is made in either part, and the theorem asserts nothing for $t_0 \notin [0, T]$ . The proof is sorry (stated, not proved).

Human review

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

View graph