HJB trajectory cost lower bound

Disproved

BertsekasDP.admissible_value_cost_lower_bound

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 along this trajectory satisfies

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

for every $t\in[t_0,T]$ , then

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

This lemma isolates the analytic trajectory-integration step of the HJB verification theorem. Continuity of $f$ and $g$ , piecewise continuity and boundedness of the control, and continuity of the state ensure that the relevant compositions are integrable away from only finitely many control discontinuities.

Preamble

import Mathlib
import Definitions.Def_BertsekasCTModel

open scoped RealInnerProductSpace

Formal statement

namespace BertsekasDP

/-- Integration of the HJB differential inequality along one admissible trajectory. -/
theorem admissible_value_cost_lower_bound {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)
    (hnonneg : ∀ t ∈ Set.Icc t₀ M.T,
      0 ≤ 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)⟫) :
    V t₀ ξ ≤ BertsekasCTCostFrom M t₀ u x := 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