Generalized Kuhn–Tucker theorem

Proved

VectorSpaceOpt.generalized_kuhn_tucker

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

convex-conegateaux-derivativekuhn-tuckerlocal-optimum

Let $X$ and $Z$ be normed real spaces, let $P$ be a convex cone in $Z$ with nonempty interior, and let $f : X → ℝ$ and $G : X → Z$ have continuous-linear Gâteaux derivatives $f^\prime$ and $G^\prime$ at $x₀$ . Assume $x₀$ is a local minimizer of $f$ subject to $G (x) ≤ₚ 0$ , and assume Luenberger regularity: $x₀$ is feasible and some linearized direction is strictly feasible. Then a cone-positive continuous functional $z₀$ exists with

f' + z₀ ∘ G' = 0, \qquad z₀(Gx₀)=0.

This capstone is the coordinate-free KKT necessary condition and reuses the cone order and dual positivity published by the earlier global-duality mission.

Preamble

import Definitions.Def_VectorSpaceOpt_cone_optimization

open Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 9, §9.4, Theorem 1. -/
theorem generalized_kuhn_tucker
    {X Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (f : X → ℝ) (G : X → Z) (x₀ : X)
    (f' : X →L[ℝ] ℝ) (G' : X →L[ℝ] Z)
    (hPint : (interior (P : Set Z)).Nonempty)
    (hf : HasGateauxDerivAt f f' x₀) (hG : HasGateauxDerivAt G G' x₀)
    (hmin : IsLocalMinOn f {x | coneLE P (G x) 0} x₀)
    (hregular : IsConeRegularAt P G G' x₀) :
    ∃ z₀ : Z →L[ℝ] ℝ, dualPositive P z₀ ∧
      f' + z₀.comp G' = 0 ∧ z₀ (G x₀) = 0 := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.4, Theorem 1, printed pp. 249–250 (physical PDF pp. 267–268). 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,Z$ be real normed spaces, not assumed complete; let $P$ be a convex cone in $Z$ with nonempty topological interior; let $f:X→ℝ$ , $G:X→Z$ , $x₀∈X$ ; and let $f':X→ℝ$ , $G':X→Z$ be continuous real-linear maps. Assume that in every direction $h$ , the curves $t↦f(x₀+th)$ and $t↦G(x₀+th)$ have derivatives $f'h$ and $G'h$ at $0$ . Assume $x₀$ is a local minimum of $f$ relative to the set of $x$ satisfying $G(x)≤_{P}0$ , where this means $-G(x)∈P$ . Also assume cone regularity at $x₀$ : $-G(x₀)∈P$ and there exists $h$ with $-(G(x₀)+G'h)∈interior(P)$ . Then there exists a continuous real-linear functional $z₀:Z→ℝ$ that is nonnegative on every element of $P$ , such that $f'+z₀∘G'$ is identically zero and $z₀(G(x₀))=0$ . No nonzeroness or uniqueness of $z₀$ is asserted.

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