Prove2Me

Abnormal equality multiplier

Proved
VectorSpaceOpt.abnormal_lagrange_multiplier

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

abnormal-multiplierclosed-rangecontinuous-duallagrange-multiplier

In the same Banach-space equality-constrained setting, retain feasibility, continuous Fréchet differentiability, and local extremality, but replace surjectivity of HprimeH^prime by the assumption that its range is closed. Then there exist a scalar r0r_0 and a continuous functional z0z_0, not both zero, such that

r0 f′+z0∘H′=0.r₀\,f' + z₀ \circ H' = 0.

The coefficient r0r₀ is allowed to vanish, so the assertion records the abnormal alternative rather than silently normalizing the objective multiplier. This corollary is not required for the regular root theorem, but it captures the exact boundary case highlighted by Luenberger and provides a reusable precursor to Fritz John and abnormal optimal-control conditions.

Preamble
import Mathlib

open Set
Formal statement
namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.3, Corollary 1. -/
theorem abnormal_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₀)
    (hrange : IsClosed (Set.range H'))
    (hextr : IsLocalExtrOn f {x | x ∈ U ∧ H x = 0} x₀) :
    ∃ (r₀ : ℝ) (z₀ : Z →L[ℝ] ℝ), (r₀, z₀) ≠ (0, 0) ∧
      r₀ • f' + z₀.comp H' = 0 := by
  sorry

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.3, Corollary 1, printed p. 244 (physical PDF p. 262). 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 XX and ZZ be real Banach spaces, U⊆XU⊆X, f:X→Rf:X→ℝ, H:X→ZH:X→Z, x0∈Xx₀∈X, and let f′:X→Rf':X→ℝ and H′:X→ZH':X→Z be continuous real-linear maps. Assume UU is open, x0∈Ux₀∈U, H(x0)=0H(x₀)=0, both ff and HH are continuously Fréchet differentiable through order one on UU, and their Fréchet derivatives at x0x₀ are respectively f′f' and H′H'. Assume also that the range of H′H' is closed and that x0x₀ is a local extremum—either a local minimum or a local maximum—of ff relative to the set of x∈Ux∈U with H(x)=0H(x)=0. Then there exist a real scalar r0r₀ and a continuous real-linear functional z0:Z→Rz₀:Z→ℝ, not simultaneously the zero scalar and zero functional, such that the continuous linear functional r0f′+z0∘H′r₀f'+z₀∘H' on XX is identically zero. No surjectivity of H′H' is assumed.

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