Measurable optimal-control framework

Definition

VectorSpaceOpt_optimal_control

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

absolute-continuitydefinitionhamiltonianmeasurabilityoptimal-control

For Euclidean state and control spaces on [t₀,t₁], an admissible pair (x,u) has fixed initial state, absolutely continuous state, almost everywhere strongly measurable control taking values in Omega almost everywhere, an a.e. state equation x' = F(x,u), and interval-integrable running cost. IsOptimalControlPair means that such a pair has no larger cost than any other admissible pair. The minimum-convention Hamiltonian is

H(x,u,λ)=⟨λ,F(x,u)⟩+ℓ(x,u).

The file also defines the interval cost, a norm-based little-o predicate, and the abstract Lagrangian used by Proposition 1. These definitions make state and control regularity explicit instead of inheriting the book's piecewise-continuity conventions informally. The measurable-control model is broader than compact-interval piecewise continuity, so the root separately assumes an a.e. norm bound for the optimal control and integrability of the two derivative-coefficient paths.

Definition code

import Mathlib

open Set Filter MeasureTheory
open scoped Interval RealInnerProductSpace

namespace VectorSpaceOpt

/-- Finite-dimensional state vectors used in the control mission. -/
abbrev OCState (n : ℕ) := EuclideanSpace ℝ (Fin n)

/-- Finite-dimensional control vectors used in the control mission. -/
abbrev OCControl (m : ℕ) := EuclideanSpace ℝ (Fin m)

/-- An admissible state-control pair for the differential system `x' = F(x,u)`. -/
def IsAdmissibleControlPair {n m : ℕ}
    (t₀ t₁ : ℝ) (F : OCState n → OCControl m → OCState n)
    (Ω : Set (OCControl m)) (xInit : OCState n)
    (ell : OCState n → OCControl m → ℝ)
    (u : ℝ → OCControl m) (x : ℝ → OCState n) : Prop :=
  x t₀ = xInit ∧
  AbsolutelyContinuousOnInterval x t₀ t₁ ∧
  AEStronglyMeasurable u (volume.restrict (Icc t₀ t₁)) ∧
  (∀ᵐ t ∂volume.restrict (Icc t₀ t₁), u t ∈ Ω) ∧
  (∀ᵐ t ∂volume.restrict (Ioo t₀ t₁), HasDerivAt x (F (x t) (u t)) t) ∧
  IntervalIntegrable (fun t => ell (x t) (u t)) volume t₀ t₁

/-- The running-cost objective of an admissible state-control pair. -/
noncomputable def controlCost {n m : ℕ} (t₀ t₁ : ℝ)
    (ell : OCState n → OCControl m → ℝ)
    (u : ℝ → OCControl m) (x : ℝ → OCState n) : ℝ :=
  ∫ t in t₀..t₁, ell (x t) (u t)

/-- Global optimality among all admissible state-control pairs. -/
def IsOptimalControlPair {n m : ℕ}
    (t₀ t₁ : ℝ) (F : OCState n → OCControl m → OCState n)
    (Ω : Set (OCControl m)) (xInit : OCState n)
    (ell : OCState n → OCControl m → ℝ)
    (u₀ : ℝ → OCControl m) (x₀ : ℝ → OCState n) : Prop :=
  IsAdmissibleControlPair t₀ t₁ F Ω xInit ell u₀ x₀ ∧
  ∀ (u : ℝ → OCControl m) (x : ℝ → OCState n),
    IsAdmissibleControlPair t₀ t₁ F Ω xInit ell u x →
      controlCost t₀ t₁ ell u₀ x₀ ≤ controlCost t₀ t₁ ell u x

/-- Luenberger's minimum-convention Hamiltonian. -/
noncomputable def controlHamiltonian {n m : ℕ}
    (F : OCState n → OCControl m → OCState n)
    (ell : OCState n → OCControl m → ℝ)
    (x : OCState n) (u : OCControl m) (lambda : OCState n) : ℝ :=
  ⟪lambda, F x u⟫ + ell x u

/-- A scalar remainder is little-o of distance to `u₀`. -/
def IsNormLittleOAt
    {U : Type*} [NormedAddCommGroup U]
    (r : U → ℝ) (u₀ : U) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∀ᶠ u in nhds u₀, ‖r u‖ ≤ ε * ‖u - u₀‖

/-- The abstract Lagrangian used in §9.6, Proposition 1. -/
def abstractControlLagrangian
    {X U : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (A : X → U → X) (g : X → U → ℝ)
    (x : X) (u : U) (lambda : X →L[ℝ] ℝ) : ℝ :=
  lambda (A x u) + g x u

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.5–§9.6, control problem and Hamiltonian setup, printed pp. 259–263 (physical PDF pp. 277–281). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

OCState and OCControl. For each natural $n$ , OCState n abbreviates the Euclidean real vector space of functions from Fin n to $ℝ$ ; for each natural $m$ , OCControl m is defined analogously. The cases $n=0$ and $m=0$ are included and give zero-dimensional one-element vector spaces.

IsAdmissibleControlPair. For naturals $n,m$ , real endpoints $t₀,t₁$ , dynamics $F$ , control set $Ω$ , initial state $x_{init}$ , running cost $ℓ$ , and total functions $u:ℝ→OCControl(m)$ and $x:ℝ→OCState(n)$ , admissibility is the conjunction of: $x(t₀)=x_{init}$ ; $x$ is absolutely continuous on the interval from $t₀$ to $t₁$ ; $u$ is almost-everywhere strongly measurable for Lebesgue measure restricted to the literal closed set $[t₀,t₁]$ ; $u(t)∈Ω$ almost everywhere for that restricted measure; for almost every $t$ under Lebesgue measure restricted to the literal open set $(t₀,t₁)$ , $x$ has derivative $F(x(t),u(t))$ at $t$ ; and $t↦ℓ(x(t),u(t))$ is interval-integrable from $t₀$ to $t₁$ . The definition itself imposes no order on $t₀,t₁$ ; in particular the literal Icc and Ioo restrictions are empty when $t₀>t₁$ , while the interval predicates retain their library-defined interval conventions.

controlCost. For any $u,x$ , admissible or not, this is the oriented interval integral $∫_{t₀}^{t₁}ℓ(x(t),u(t))dt$ . It is a total real-valued definition.

IsOptimalControlPair. A pair $(u₀,x₀)$ is optimal exactly when it is admissible and, for every pair of total functions $(u,x)$ that is admissible for the same data, its control cost is no larger than that pair's cost. This is global comparison over all admissible pairs, not merely local comparison.

controlHamiltonian. For $x∈OCState(n)$ , $u∈OCControl(m)$ , and $λ∈OCState(n)$ , the Hamiltonian is $⟨λ,F(x,u)⟩+ℓ(x,u)$ . No feasibility or regularity is part of this definition.

IsNormLittleOAt. For a normed additive commutative group $U$ , $r:U→ℝ$ , and $u₀∈U$ , this means: for every real $ε>0$ , eventually as $u$ tends to $u₀$ , $|r(u)|≤ε‖u-u₀‖$ . The eventual quantifier is the neighborhood filter at $u₀$ ; no continuity of $r$ is separately required, and the condition in particular forces $r(u₀)=0$ .

abstractControlLagrangian. For a real normed space $X$ , an arbitrary type $U$ , maps $A:X→U→X$ and $g:X→U→ℝ$ , $x∈X$ , $u∈U$ , and a continuous real-linear functional $λ:X→ℝ$ , its value is $λ(A(x,u))+g(x,u)$ .

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph