Pontryagin minimum principle

Proved

VectorSpaceOpt.pontryagin_minimum_principle

by wenxinzhang · Aug 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

almost-everywherecostateminimum-principlepontryaginsource-erratum

Fix a positive-length interval, continuously state-differentiable dynamics $F$ and running cost $\ell$ , continuous state derivatives, interval integrability of those derivative coefficients along the optimal path, an a.e. norm bound for the optimal control, and a uniform Lipschitz bound for the dynamics. If $(x₀,u₀)$ is an optimal admissible state-control pair, then there exists an absolutely continuous costate $\lambda$ with $\lambda (t₁) = 0$ . Its adjoint equation holds almost everywhere in weak inner-product form, and almost everywhere

H(x₀(t),u₀(t),λ(t)) ≤ H(x₀(t),v,λ(t)) \quad ∀v∈Ω.

The a.e. qualifier is a deliberate correction to the book's false all-times wording for piecewise-continuous controls. The statement includes measurable controls, absolutely continuous states and costate, and joint continuity and interval integrability of the state derivatives needed along the optimal path. The explicit a.e. control bound restores the compact-interval boundedness inherited from the source piecewise-continuous model and supplies local domination for state perturbations.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set MeasureTheory
open scoped RealInnerProductSpace

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.6, Theorem 1, repaired from `∀ t` to an a.e. conclusion. -/
theorem pontryagin_minimum_principle
    {n m : ℕ} (t₀ t₁ : ℝ) (ht : t₀ < t₁)
    (F : OCState n → OCControl m → OCState n)
    (ell : OCState n → OCControl m → ℝ)
    (Fx : OCState n → OCControl m → (OCState n →L[ℝ] OCState n))
    (ellx : OCState n → OCControl m → (OCState n →L[ℝ] ℝ))
    (Omega : Set (OCControl m)) (xInit : OCState n)
    (u₀ : ℝ → OCControl m) (x₀ : ℝ → OCState n)
    (hFx : ∀ x u, HasFDerivAt (fun y => F y u) (Fx x u) x)
    (hellx : ∀ x u, HasFDerivAt (fun y => ell y u) (ellx x u) x)
    (hFCont : Continuous (Function.uncurry F))
    (hellCont : Continuous (Function.uncurry ell))
    (hFxCont : Continuous (Function.uncurry Fx))
    (hellxCont : Continuous (Function.uncurry ellx))
    (hFxPathInt : IntervalIntegrable (fun t => Fx (x₀ t) (u₀ t)) volume t₀ t₁)
    (hellxPathInt : IntervalIntegrable (fun t => ellx (x₀ t) (u₀ t)) volume t₀ t₁)
    (hu₀Bound : ∃ C : ℝ, ∀ᵐ t ∂volume.restrict (Icc t₀ t₁), ‖u₀ t‖ ≤ C)
    (hLip : ∃ M : ℝ, 0 ≤ M ∧ ∀ x y u v,
      ‖F x u - F y v‖ ≤ M * (‖x - y‖ + ‖u - v‖))
    (hopt : IsOptimalControlPair t₀ t₁ F Omega xInit ell u₀ x₀) :
    ∃ lambda : ℝ → OCState n,
      lambda t₁ = 0 ∧
      AbsolutelyContinuousOnInterval lambda t₀ t₁ ∧
      (∀ᵐ t ∂volume.restrict (Ioo t₀ t₁),
        ∃ dlambda : OCState n, HasDerivAt lambda dlambda t ∧
          ∀ h : OCState n,
            ⟪-dlambda, h⟫ =
              ⟪lambda t, Fx (x₀ t) (u₀ t) h⟫ + ellx (x₀ t) (u₀ t) h) ∧
      (∀ᵐ t ∂volume.restrict (Icc t₀ t₁),
        ∀ v : OCControl m, v ∈ Omega →
          controlHamiltonian F ell (x₀ t) (u₀ t) (lambda t) ≤
            controlHamiltonian F ell (x₀ t) v (lambda t)) := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.6, Theorem 1, printed pp. 263–264 (physical PDF pp. 281–282), with the Hamiltonian quantifier repaired from every time to almost every time. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

View graph