Pontryagin Minimum Principle (Prop. 3.3.1)

Proved

BertsekasDP.pontryagin_minimum_principle

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

minimumprinciplenecessaryconditionspontryagin

Proposition 3.3.1 (Pontryagin Minimum Principle). Consider the continuous-time problem of minimizing $h(x(T)) + \int_0^T g(x,u)\,dt$ subject to $\dot x = f(x,u)$ , $x(0) = x_0$ and $u(t) \in U$ , with $f$ , $g$ and $h$ continuously differentiable. Let $\{u^*(t) \mid t \in [0,T]\}$ be an optimal admissible control trajectory and $\{x^*(t)\}$ the corresponding state trajectory. Then there is an adjoint trajectory $p$ , continuous on $[0,T]$ , satisfying the adjoint equation and its terminal condition

\dot p(t) \;=\; -\nabla_x H\bigl(x^*(t), u^*(t), p(t)\bigr), \qquad p(T) \;=\; \nabla h\bigl(x^*(T)\bigr),

such that the control minimizes the Hamiltonian pointwise,

u^*(t) \;\in\; \arg\min_{u \in U} \; H\bigl(x^*(t), u, p(t)\bigr),

and the Hamiltonian is constant along the optimal trajectory,

H\bigl(x^*(t), u^*(t), p(t)\bigr) \;=\; c \qquad \text{for all } t,

for some constant $c$ . Here $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ .

The Minimum Principle converts an optimization over a function space into a two-point boundary value problem in $2n$ ordinary differential equations — the basis of shooting methods and of every bang-bang analysis. Its conditions are necessary, not sufficient: a trajectory satisfying them need not be optimal, and further argument (existence plus uniqueness of the candidate, or convexity) is needed to conclude optimality.

Formalization Note The three conditions hold off a common finite exceptional set, which is where the piecewise continuous control switches; this is the precise reading of the source's "for all $t \in [0,T]$ " in the presence of switching. Constancy of the Hamiltonian uses time-independence of $f$ and $g$ , as the source notes it may fail otherwise. Uniqueness of $p$ is not asserted, and the terminal condition fixes the cost multiplier at $1$ , so no abnormal multiplier appears.

Preamble

import Mathlib
import Definitions.Def_BertsekasCTModel

Formal statement

namespace BertsekasDP

theorem pontryagin_minimum_principle {n m : ℕ} (M : BertsekasCTModel n m)
    (hf : ContDiff ℝ 1 (Function.uncurry M.f))
    (hg : ContDiff ℝ 1 (Function.uncurry M.g))
    (hh : ContDiff ℝ 1 M.h)
    (ustar : ℝ → EuclideanSpace ℝ (Fin m))
    (xstar : ℝ → EuclideanSpace ℝ (Fin n))
    (hadm : BertsekasCTAdmissibleFrom M 0 M.x0 ustar xstar)
    (hopt : ∀ u x, BertsekasCTAdmissibleFrom M 0 M.x0 u x →
      BertsekasCTCostFrom M 0 ustar xstar ≤ BertsekasCTCostFrom M 0 u x) :
    ∃ (p : ℝ → EuclideanSpace ℝ (Fin n)) (F : Finset ℝ) (c : ℝ),
      ContinuousOn p (Set.Icc 0 M.T) ∧
      p M.T = gradient M.h (xstar M.T) ∧
      (∀ t ∈ Set.Icc 0 M.T \ (F : Set ℝ),
        HasDerivAt p
          (-gradient (fun y => BertsekasHamiltonian M y (ustar t) (p t)) (xstar t))
          t) ∧
      (∀ t ∈ Set.Icc 0 M.T \ (F : Set ℝ),
        IsMinOn (fun u => BertsekasHamiltonian M (xstar t) u (p t)) M.U (ustar t)) ∧
      (∀ t ∈ Set.Icc 0 M.T \ (F : Set ℝ),
        BertsekasHamiltonian M (xstar t) (ustar t) (p t) = c) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 3.3.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$ ). Assume:

$f : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^n$ and $g : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}$ are jointly $C^1$ in the pair $(x, u)$ , and $h : \mathbb{R}^n \to \mathbb{R}$ is $C^1$ ;
$(u^*, x^*)$ , with $u^* : \mathbb{R} \to \mathbb{R}^m$ and $x^* : \mathbb{R} \to \mathbb{R}^n$ , is admissible from $(0, x_0)$ in this bundle's sense: $u^*(t) \in U$ for all $t \in [0, T]$ ; the image $u^*([0, T])$ is bounded and $u^*$ is continuous on $[0, T]$ minus some finite set; $x^*$ is continuous on $[0, T]$ with $x^*(0) = x_0$ ; and there is a finite set off which, on $[0, T]$ , $x^*$ has two-sided derivative $f(x^*(t), u^*(t))$ ;
optimality: for every pair $(u, x)$ admissible from $(0, x_0)$ in the same sense,

h(x^*(T)) + \int_0^T g(x^*(t), u^*(t))\,dt \;\le\; h(x(T)) + \int_0^T g(x(t), u(t))\,dt,

i.e. $\mathrm{BertsekasCTCostFrom}(M, 0, u^*, x^*) \le \mathrm{BertsekasCTCostFrom}(M, 0, u, x)$ (global optimality over all admissible pairs; recall each interval integral silently equals $0$ when its integrand is not integrable).

Conclusion. There exist a function $p : \mathbb{R} \to \mathbb{R}^n$ (defined on all of $\mathbb{R}$ ; unconstrained outside the conditions below), a single finite set $F \subseteq \mathbb{R}$ shared by the three "off- $F$ " conditions below, and a constant $c \in \mathbb{R}$ , such that, writing $H(x, u, p) = g(x, u) + \langle p, f(x, u)\rangle$ for this bundle's Hamiltonian:

$p$ is continuous on $[0, T]$ ;
$p(T) = \nabla h(x^*(T))$ (Mathlib total gradient; well-defined classically since $h$ is $C^1$ );
adjoint equation: for every $t \in [0, T] \setminus F$ , $p$ has the two-sided derivative

p'(t) = -\,\nabla_y \big[\, g(y, u^*(t)) + \langle p(t),\, f(y, u^*(t))\rangle \,\big]\Big|_{y = x^*(t)}

at $t$ — the gradient is taken in the state variable only, with the control frozen at $u^*(t)$ and the costate frozen at $p(t)$ ; being a two-sided derivative, at an endpoint $0$ or $T$ not excluded by $F$ this constrains $p$ outside $[0, T]$ as well; 4. minimum condition: for every $t \in [0, T] \setminus F$ , $u^*(t)$ is a minimum point on $U$ of the map $u \mapsto H(x^*(t), u, p(t))$ , i.e. for every $u \in U$ :

g(x^*(t), u^*(t)) + \langle p(t), f(x^*(t), u^*(t))\rangle \;\le\; g(x^*(t), u) + \langle p(t), f(x^*(t), u)\rangle

(non-strict; this does not by itself assert $u^*(t) \in U$ , though admissibility separately gives $u^*(t) \in U$ for $t \in [0,T]$ ); 5. constancy of the Hamiltonian: for every $t \in [0, T] \setminus F$ ,

g(x^*(t), u^*(t)) + \langle p(t),\, f(x^*(t), u^*(t))\rangle = c.

All three pointwise conditions 3–5 are claimed only off the same finite exceptional set $F$ , which the existential quantifier lets be as large (but finite) as needed; nothing is claimed at points of $F$ or outside $[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