Prove2Me

Stationarity on the constraint tangent kernel

Proved
VectorSpaceOpt.constrained_extremum_tangent_stationary

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

banach-spaceconstrained-extremumstationaritytangent-space

Let XX and ZZ be real Banach spaces, let f ⁣:X→Rf \colon X \to \mathbb R and H ⁣:X→ZH \colon X \to Z be continuously Fréchet differentiable on an open set UU, and let x0∈Ux_0 \in U satisfy H(x0)=0H(x_0) = 0. Write f′f^\prime and H′H^\prime for their derivatives at x0x_0, and assume H′H^\prime is onto. If x0x_0 is a local minimum or local maximum of ff relative to {x∣x∈U∨H(x)=0}\{x | x \in U \vee H (x) = 0\}, then

H′(h)=0⟹f′(h)=0H^\prime(h)=0 \quad\Longrightarrow\quad f^\prime(h)=0

for every direction hh. This identifies the kernel of the linearized constraint as the true tangent test space and is the immediate analytic input to the multiplier factorization.

Preamble
import Mathlib

open Set
Formal statement
namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.3, Lemma 1. -/
theorem constrained_extremum_tangent_stationary
    {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₀) :
    ∀ h : X, H' h = 0 → f' h = 0 := by
  sorry

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.3, Lemma 1, printed p. 242 (physical PDF p. 260). 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, ff and HH are continuously Fréchet differentiable through order one on UU, their Fréchet derivatives at x0x₀ are f′f' and H′H', H′H' is surjective, and x0x₀ is a local minimum or local maximum of ff relative to the points x∈Ux∈U satisfying H(x)=0H(x)=0. Then every direction h∈Xh∈X in the kernel of H′H' also lies in the kernel of f′f': H′h=0H'h=0 implies f′h=0f'h=0. The conclusion quantifies over all hh, including h=0h=0.

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