HJB trajectory cost equality

Disproved

BertsekasDP.admissible_value_cost_eq

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

continuous-timehjb-equationoptimal-controltrajectory-integration

Suppose $f$ and $g$ are jointly continuous, $V$ is continuously differentiable, and $V(T,x)=h(x)$ . Fix one admissible trajectory $(u,x)$ from $(t_0,\xi)$ . If the HJB expression vanishes along the trajectory,

g(x(t),u(t))+\partial_tV(t,x(t))+\langle\nabla_xV(t,x(t)),f(x(t),u(t))\rangle=0

for every $t\in[t_0,T]$ , then its total cost equals the candidate value:

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

This is the equality form of the trajectory-integration step used to certify a control that attains the HJB infimum.

Preamble

import Mathlib
import Definitions.Def_BertsekasCTModel

open scoped RealInnerProductSpace

Formal statement

namespace BertsekasDP

/-- Integration of the HJB equality along one admissible trajectory. -/
theorem admissible_value_cost_eq {n m : ℕ} (M : BertsekasCTModel n m)
    (hf : Continuous (Function.uncurry M.f))
    (hg : Continuous (Function.uncurry M.g))
    (V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ)
    (hV : ContDiff ℝ 1 (Function.uncurry V))
    (hbdry : ∀ x, V M.T x = M.h x)
    (t₀ : ℝ) (ξ : EuclideanSpace ℝ (Fin n))
    (u : ℝ → EuclideanSpace ℝ (Fin m))
    (x : ℝ → EuclideanSpace ℝ (Fin n))
    (hadm : BertsekasCTAdmissibleFrom M t₀ ξ u x)
    (hzero : ∀ t ∈ Set.Icc t₀ M.T,
      M.g (x t) (u t) + deriv (fun s => V s (x t)) t +
        ⟪gradient (V t) (x t), M.f (x t) (u t)⟫ = 0) :
    BertsekasCTCostFrom M t₀ u x = 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 and the integration argument in Section 3.2; regularity assumptions from Section 3.1, p. 107.

View graph