Equality-constrained Lagrange multiplier

Proved

VectorSpaceOpt.equality_lagrange_multiplier

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

banach-spaceequality-constraintlagrange-multiplierlocal-optimum

Let $X$ and $Z$ be real Banach spaces, $U \subseteq X$ open, and $f \colon X \to \mathbb R$ , $H \colon X \to Z$ continuously Fréchet differentiable on $U$ . Suppose $x₀ \in U$ , $H (x₀) = 0$ , the derivative $H^\prime$ at $x₀$ is surjective, and $x₀$ is a local extremum of $f$ on the feasible level set. If $f^\prime$ is the derivative of $f$ at $x₀$ , then a continuous multiplier $z₀ \colon Z \to L[ℝ] ℝ$ exists with

f' + z₀ \circ H' = 0.

This is the mission capstone: it converts tangent stationarity into a coordinate-free multiplier equation and supplies the regular Banach-space equality rule used throughout later vector-space optimization.

Preamble

import Mathlib

open Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.3, Theorem 1. -/
theorem equality_lagrange_multiplier
    {X Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z] [CompleteSpace Z]
    (U : Set X) (f : X → ℝ) (H : X → Z) (x₀ : X)
    (f' : X →L[ℝ] ℝ) (H' : X →L[ℝ] Z)
    (hU : IsOpen U) (hx₀ : x₀ ∈ U) (hfeas : H x₀ = 0)
    (hf : ContDiffOn ℝ 1 f U) (hH : ContDiffOn ℝ 1 H U)
    (hf' : HasFDerivAt f f' x₀) (hH' : HasFDerivAt H H' x₀)
    (hregular : Function.Surjective H')
    (hextr : IsLocalExtrOn f {x | x ∈ U ∧ H x = 0} x₀) :
    ∃ z₀ : Z →L[ℝ] ℝ, f' + z₀.comp H' = 0 := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.3, Theorem 1, printed p. 243 (physical PDF p. 261). 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$ and $Z$ be real Banach spaces, $U⊆X$ , $f:X→ℝ$ , $H:X→Z$ , $x₀∈X$ , and let $f':X→ℝ$ and $H':X→Z$ be continuous real-linear maps. Assume $U$ is open, $x₀∈U$ , $H(x₀)=0$ , $f$ and $H$ are continuously Fréchet differentiable through order one on $U$ , their Fréchet derivatives at $x₀$ are $f'$ and $H'$ , $H'$ is surjective, and $x₀$ is a local minimum or local maximum of $f$ relative to the points $x∈U$ satisfying $H(x)=0$ . Then there exists a continuous real-linear functional $z₀:Z→ℝ$ such that $f'+z₀∘H'$ is the zero continuous linear functional on $X$ . No nonzero condition or uniqueness condition is imposed on $z₀$ .

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