Vector Space Methods XII: Pontryagin Minimum PrincipleTextbook
## Motivation [Pontryagin's principle as presented by Luenberger](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement. ## Setting Fix `t₀ < t₁`, a finite-dimensional **Euclidean state space** `OCState n`, a Euclidean control space `OCControl m`, and a permitted-control set `Omega`. A state-control pair `(x,u)` is **admissible** when `x t₀ = xInit`, the state is **absolutely continuous** on the interval, the control is **almost everywhere strongly measurable** and lies in `Omega` almost everywhere, the differential equation `x' = F(x,u)` holds almost everywhere in the interior, and the running cost is interval integrable. An **optimal pair** globally minimizes the interval integral among all admissible pairs. The dynamics `F` and running cost `ell` are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives `Fx` and `ellx` vary continuously. A global Lipschitz estimate controls changes of `F` in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths `Fx (x₀ t) (u₀ t)` and `ellx (x₀ t) (u₀ t)` are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention, $$ H(x,u,\lambda)=\langle \lambda,F(x,u)\rangle+\ell(x,u). $$ ## Formalization targets The root `VectorSpaceOpt.pontryagin_minimum_principle` asserts the existence of an absolutely continuous costate `lambda` with terminal value `lambda t₁ = 0`. Almost everywhere it satisfies the weak inner-product form of $$ -\dot\lambda(t)=D_xF(x₀(t),u₀(t))^*\lambda(t)+D_x\ell(x₀(t),u₀(t)), $$ and almost everywhere on the control interval it satisfies $$ H(x₀(t),u₀(t),\lambda(t)) \le H(x₀(t),v,\lambda(t)) \quad\text{for every }v\in\Omega. $$ Two milestones capture source dependencies. `control_state_lipschitz_estimate` is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. `adjoint_lagrangian_comparison` formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder. ## Significance This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted. The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers. ## Difficulty The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder. ## Formalization scope The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on `Icc t₀ t₁`, restoring the compact-interval boundedness used by the source. The maps `F`, `ell`, `Fx`, and `ellx` are jointly continuous; state derivatives are supplied by `HasFDerivAt`; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length. There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every `t`, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on `Icc t₀ t₁`; an alternative source-faithful repair would assert the inequality at every continuity point of `u₀`. The mission does not claim existence of an optimal pair, compactness of `Omega`, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem. ## Selected references - David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.6, Proposition 1 and Theorem 1, pp. 262–264, including the printed all-times wording and its proof context. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf - Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (interval integration, absolute continuity, Euclidean spaces, Fréchet derivatives, ODE estimates, and a.e. measurability).