Needle variation: admissible trajectories and first-order cost

Proved

VectorSpaceOpt.needle_variation_cost_limit

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

almost-everywherefirst-variationneedle-variationoptimal-control

Fix an admissible state-control pair $(x_0,u_0)$ on $[t_0,t_1]$ , with $t_0<t_1$ , and an absolutely continuous costate $\lambda$ satisfying the adjoint equation almost everywhere and $\lambda(t_1)=0$ . Assume jointly continuous dynamics $F$ , running cost $\ell$ , and their state derivatives; differentiability in the state; interval integrability of both derivative paths; an essential bound for $u_0$ ; and a global joint Lipschitz bound for $F$ .

For each fixed permitted value $v\in\Omega$ , at almost every interior time $t$ there is a family of state trajectories $x_\varepsilon$ such that, for every sufficiently small positive $\varepsilon$ , the control

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

and $x_\varepsilon$ form an admissible pair with the same initial state, and

\lim_{\varepsilon\downarrow0} \frac{J(x_\varepsilon,u_{\varepsilon,t,v})-J(x_0,u_0)}{\varepsilon} = H(x_0(t),v,\lambda(t))-H(x_0(t),u_0(t),\lambda(t)).

Here $J$ is the integral running cost and $H(x,u,\lambda)=\langle\lambda,F(x,u)\rangle+\ell(x,u)$ . This isolates the analytic first-variation calculation from the optimization argument: the reference pair is admissible but need not be optimal. The exceptional null set may depend on the fixed value $v$ .

Formalization Note. This is the right-needle specialization of the source's first-order Hamiltonian comparison, with an almost-everywhere limit appropriate for the mission's measurable-control formulation. The existence of admissible perturbed states and the derivative limit are conclusions, not added assumptions.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

open Set Filter MeasureTheory
open scoped RealInnerProductSpace Topology

open VectorSpaceOpt

Formal statement

theorem VectorSpaceOpt.needle_variation_cost_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)
    (hLip : ∃ M : ℝ, 0 ≤ M ∧ ∀ x y u v,
      ‖F x u - F y v‖ ≤ M * (‖x - y‖ + ‖u - v‖))
    (hadm : IsAdmissibleControlPair t₀ t₁ F Omega xInit ell u₀ x₀)
    (lambda : ℝ → OCState n)
    (hlambdaTerm : lambda t₁ = 0)
    (hlambdaAC : AbsolutelyContinuousOnInterval lambda t₀ t₁)
    (hadjoint : ∀ᵐ 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)
    (v : OCControl m) (hv : v ∈ Omega) :
    ∀ᵐ t ∂volume.restrict (Ioo t₀ t₁),
      ∃ xPert : ℝ → ℝ → OCState n,
        (∀ᶠ ε : ℝ in 𝓝[>] (0 : ℝ),
          IsAdmissibleControlPair t₀ t₁ F Omega xInit ell
            (fun s => if s ∈ Icc t (t + ε) then v else u₀ s) (xPert ε)) ∧
        Tendsto
          (fun ε : ℝ =>
            (controlCost t₀ t₁ ell
              (fun s => if s ∈ Icc t (t + ε) then v else u₀ s) (xPert ε) -
              controlCost t₀ t₁ ell u₀ x₀) / ε)
          (𝓝[>] (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, Proposition 1 and proof of Theorem 1, pp. 262–264, especially equation (9) and the localized constant-control replacement on p. 264. https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf . This child specializes that comparison to right needles and states its Lebesgue-point, almost-everywhere form under the explicit measurable-control hypotheses of VectorSpaceOpt.pontryagin_minimum_principle; it does not repeat the source's all-times assertion.

View graph