First-order limit of the Hamiltonian integral under a needle variation

Proved

VectorSpaceOpt.needle_hamiltonian_integral_limit

by davidnet · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

almost-everywherefirst-variationlebesgue-pointneedle-variationoptimal-control

Let $t_0<t_1$ and let $(u_0,x_0)$ be an admissible pair on $[t_0,t_1]$ with $u_0$ essentially bounded. Assume that the dynamics $F$ and the running cost $\ell$ are jointly continuous and differentiable in the state, with jointly continuous state derivatives $F_x$ and $\ell_x$ , and that the derivative paths $s\mapsto F_x(x_0(s),u_0(s))$ and $s\mapsto\ell_x(x_0(s),u_0(s))$ are integrable on $[t_0,t_1]$ . Let $\lambda$ be continuous on $[t_0,t_1]$ and fix a value $v\in\mathbb R^m$ . For $t\in(t_0,t_1)$ and $\varepsilon>0$ write $u_\varepsilon$ for the right needle

u_\varepsilon(s)=\begin{cases}v,&s\in[t,t+\varepsilon],\\ u_0(s),&s\notin[t,t+\varepsilon].\end{cases}

Then for almost every $t\in(t_0,t_1)$ the following holds. Whenever $(x_\varepsilon)$ is a family of states and $K$ is a constant such that, for all sufficiently small $\varepsilon>0$ , the pair $(u_\varepsilon,x_\varepsilon)$ is admissible and

\sup_{s\in[t_0,t_1]}\|x_\varepsilon(s)-x_0(s)\|\le K\varepsilon ,

one has

\lim_{\varepsilon\downarrow 0}\frac{1}{\varepsilon}\Bigl(\int_{t_0}^{t_1}\bigl[H(x_\varepsilon,u_\varepsilon,\lambda)-H(x_0,u_0,\lambda)\bigr]ds-\int_{t_0}^{t_1}\bigl[\langle\lambda,F_x(x_0,u_0)(x_\varepsilon-x_0)\rangle+\ell_x(x_0,u_0)(x_\varepsilon-x_0)\bigr]ds\Bigr)=H(x_0(t),v,\lambda(t))-H(x_0(t),u_0(t),\lambda(t)),

where $H(x,u,\lambda)=\langle\lambda,F(x,u)\rangle+\ell(x,u)$ is the Hamiltonian and every integrand is evaluated at the time $s$ .

This is the localized constant-control replacement in Luenberger's proof of Theorem 1, made quantitative for measurable controls. On the needle the integrand averages to the Hamiltonian jump at Lebesgue points of $s\mapsto H(x_0(s),u_0(s),\lambda(s))$ ; off the needle the integrand is the Taylor remainder of $H$ in the state, which is uniformly $o(\|x_\varepsilon-x_0\|)=o(\varepsilon)$ by continuity of $F_x$ and $\ell_x$ on a compact set; and the linearized term on the needle is $O(\varepsilon^2)$ at Lebesgue points of the derivative paths. The exceptional null set of times depends only on the reference pair, $\lambda$ and $v$ , not on the family $(x_\varepsilon)$ . Combined with the adjoint identity for the cost difference, this gives the first-order cost expansion of a needle variation.

Formalization Note. The null set is quantified first; the family $x_\varepsilon$ , the constant $K$ and the eventual admissibility and closeness hypotheses are quantified inside it. Only continuity of $\lambda$ is assumed; the adjoint equation and the terminal condition are not needed for this limit.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set Filter MeasureTheory
open scoped RealInnerProductSpace Topology

open VectorSpaceOpt

Formal statement

theorem VectorSpaceOpt.needle_hamiltonian_integral_limit
    {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)
    (hadm : IsAdmissibleControlPair t₀ t₁ F Omega xInit ell u₀ x₀)
    (lambda : ℝ → OCState n)
    (hlambdaCont : ContinuousOn lambda (Icc t₀ t₁))
    (v : OCControl m) :
    ∀ᵐ t ∂volume.restrict (Ioo t₀ t₁),
      ∀ (xPert : ℝ → ℝ → OCState n) (K : ℝ),
        (∀ᶠ ε : ℝ in 𝓝[>] (0 : ℝ),
          IsAdmissibleControlPair t₀ t₁ F Omega xInit ell
            (fun s => if s ∈ Icc t (t + ε) then v else u₀ s) (xPert ε) ∧
          ∀ s ∈ Icc t₀ t₁, ‖xPert ε s - x₀ s‖ ≤ K * ε) →
        Tendsto
          (fun ε : ℝ =>
            ((∫ s in t₀..t₁,
                (controlHamiltonian F ell (xPert ε s)
                    (if s ∈ Icc t (t + ε) then v else u₀ s) (lambda s) -
                  controlHamiltonian F ell (x₀ s) (u₀ s) (lambda s))) -
              ∫ s in t₀..t₁,
                (⟪lambda s, Fx (x₀ s) (u₀ s) (xPert ε s - x₀ s)⟫ +
                  ellx (x₀ s) (u₀ s) (xPert ε s - x₀ s))) / ε)
          (𝓝[>] (0 : ℝ))
          (𝓝 (controlHamiltonian F ell (x₀ t) v (lambda t) -
            controlHamiltonian F ell (x₀ t) (u₀ t) (lambda t))) := by
  sorry

Source

D. G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), §9.6, proof of Theorem 1, p. 264: the control equal to ū on a short interval [t′,t″] and to u₀ elsewhere, and the estimate J(u₀) − J(u) > ε(t″ − t′) + o(‖u − u₀‖) derived from equation (9); Proposition 1, p. 262, for the state remainder. https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf . The almost-everywhere form replaces the source's continuity of piecewise-continuous controls by the Lebesgue differentiation theorem at Lebesgue points of the Hamiltonian path.

View graph