Adjoint Lagrangian first-order comparison

Open

VectorSpaceOpt.adjoint_lagrangian_comparison

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

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

Read-back

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

Let $X$ be a real Banach space and $U$ a real normed space, not assumed complete. Fix $Ω⊆U$ , maps $A:X→U→X$ and $g:X→U→ℝ$ , a state selection $x_{of}:U→X$ , assignments $A_x(x,v):X→X$ and $g_x(x,v):X→ℝ$ of continuous real-linear maps, a point $u∈U$ , and a continuous real-linear functional $λ:X→ℝ$ . Assume $A(x_{of}(v),v)=0$ for every $v∈U$ ; for every $x,v$ , $A_x(x,v)$ and $g_x(x,v)$ are the Fréchet derivatives at $x$ of the first-argument maps $y↦A(y,v)$ and $y↦g(y,v)$ ; and the operator-valued maps $(x,v)↦A_x(x,v)$ and $(x,v)↦g_x(x,v)$ are continuous on $X×U$ . Assume there is a real $K≥0$ such that $‖x_{of}(u)-x_{of}(v)‖≤K‖u-v‖$ for every $v∈U$ , and assume the adjoint functional equation $λ∘A_x(x_{of}(u),u)+g_x(x_{of}(u),u)=0$ . Then there exists $r:U→ℝ$ such that, for every $ε>0$ , eventually near $u$ one has $|r(v)|≤ε‖v-u‖$ , and for every $v∈Ω$ , $g(x_{of}(u),u)-g(x_{of}(v),v)=[λ(A(x_{of}(u),u))+g(x_{of}(u),u)]-[λ(A(x_{of}(u),v))+g(x_{of}(u),v)]+r(v)$ . The distinguished $u$ is not required to lie in $Ω$ ; if $Ω$ is empty, the displayed comparison is vacuous but the little-o remainder must still exist.

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