Adjoint Lagrangian first-order comparison

Proved

VectorSpaceOpt.adjoint_lagrangian_comparison

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

adjointimplicit-statelagrangianlittle-o

Let an implicit state map xOf solve A (xOf v) v = 0. Assume A and the objective g are Fréchet differentiable in the state with continuously varying derivatives, and assume xOf is Lipschitz at the reference control u. If a continuous functional lambda satisfies the adjoint identity lambda ∘ Aₓ + gₓ = 0 at (xOf u,u), then there is a remainder r that is little-o of ‖v-u‖ and

g(x(u),u)-g(x(v),v)=L(x(u),u,λ)-L(x(u),v,λ)+r(v)

for every permitted v. This makes the source's unspecified asymptotic term precise and isolates the multiplier comparison underlying the control variation.

Preamble

import Definitions.Def_VectorSpaceOpt_optimal_control

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.6, Proposition 1, with little-o made explicit. -/
theorem adjoint_lagrangian_comparison
    {X U : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup U] [NormedSpace ℝ U]
    (Omega : Set U) (A : X → U → X) (g : X → U → ℝ)
    (xOf : U → X) (Ax : X → U → (X →L[ℝ] X))
    (gx : X → U → (X →L[ℝ] ℝ)) (u : U)
    (lambda : X →L[ℝ] ℝ)
    (hstate : ∀ v : U, A (xOf v) v = 0)
    (hAx : ∀ (x : X) (v : U), HasFDerivAt (fun y => A y v) (Ax x v) x)
    (hgx : ∀ (x : X) (v : U), HasFDerivAt (fun y => g y v) (gx x v) x)
    (hAxCont : Continuous (fun p : X × U => Ax p.1 p.2))
    (hgxCont : Continuous (fun p : X × U => gx p.1 p.2))
    (hxLip : ∃ K : ℝ, 0 ≤ K ∧ ∀ v : U, ‖xOf u - xOf v‖ ≤ K * ‖u - v‖)
    (hadjoint : lambda.comp (Ax (xOf u) u) + gx (xOf u) u = 0) :
    ∃ r : U → ℝ, IsNormLittleOAt r u ∧
      ∀ v ∈ Omega,
        g (xOf u) u - g (xOf v) v =
          abstractControlLagrangian A g (xOf u) u lambda -
            abstractControlLagrangian A g (xOf u) v lambda + r v := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.6, Proposition 1, printed p. 262 (physical PDF p. 280). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

View graph