Motivation

The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.

Setting

Minimize, over admissible pairs, the cost

$$h(x(T)) + \int_0^T g(x(t), u(t))\,dt \quad\text{s.t.}\quad \dot x(t) = f(x(t), u(t)),\; x(0) = x_0,\; u(t) \in U \subseteq \mathbb{R}^m,$$

with $f, g, h$ continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on $[0,T]$ — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start $(t_0, \xi)$). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (BertsekasHamiltonian).

Target

For an optimal admissible pair $(u^*, x^*)$: there exist an adjoint $p$ and a constant $c$ with

$$\dot p(t) = -\nabla_x H(x^*(t), u^*(t), p(t)), \quad p(T) = \nabla h(x^*(T)),$$ $$u^*(t) \in \arg\min_{u \in U} H(x^*(t), u, p(t)), \qquad H(x^*(t), u^*(t), p(t)) = c,$$

away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).

The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$.

Significance

The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.

Difficulty

For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.

Formalization scope

States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set — no compactness or convexity is assumed in the goal.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
• W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7