Separation of the linearized KKT system

Proved

VectorSpaceOpt.kkt_linearized_separator

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

continuous-linear-functionaldual-conekktseparation

Let P be a convex cone with nonempty interior in a normed real space Z. Fix a feasible constraint value, objective derivative f', and constraint derivative G'. Assume a direction makes the linearized constraint strictly feasible, while no direction both makes it strictly feasible and gives negative objective derivative. Then there is a continuous linear functional z₀ that is nonnegative on P and satisfies

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

This milestone packages the functional-analytic separating-hyperplane core of Luenberger's theorem. It is independent of the nonlinear origin of f' and G', so it can be reused for other cone-linearized necessary conditions and alternative differentiability frameworks.

Preamble

import Definitions.Def_VectorSpaceOpt_cone_optimization

open Set

Formal statement

namespace VectorSpaceOpt

/-- The separating-hyperplane core of Luenberger, §9.4, Theorem 1. -/
theorem kkt_linearized_separator
    {X Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (xConstraint : Z)
    (f' : X →L[ℝ] ℝ) (G' : X →L[ℝ] Z)
    (hPint : (interior (P : Set Z)).Nonempty)
    (hfeas : coneLE P xConstraint 0)
    (hregular : ∃ h : X, coneLT P (xConstraint + G' h) 0)
    (hNoDescent : ¬ ∃ h : X, f' h < 0 ∧ coneLT P (xConstraint + G' h) 0) :
    ∃ z₀ : Z →L[ℝ] ℝ, dualPositive P z₀ ∧
      f' + z₀.comp G' = 0 ∧ z₀ xConstraint = 0 := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.4, separating-hyperplane portion of 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, $P$ a convex cone in $Z$ , $c∈Z$ , and $f':X→ℝ$ , $G':X→Z$ continuous real-linear maps. Assume $interior(P)$ is nonempty, $c≤_{P}0$ (equivalently $-c∈P$ ), and there exists $h∈X$ such that $c+G'h<_{P}0$ (equivalently $-(c+G'h)∈interior(P)$ ). Assume moreover that there does not exist any $h∈X$ satisfying both $f'h<0$ and $-(c+G'h)∈interior(P)$ . Then there exists a continuous real-linear $z₀:Z→ℝ$ , nonnegative on all of $P$ , for which $f'+z₀∘G'=0$ and $z₀(c)=0$ . No derivatives of nonlinear maps, completeness assumptions, or uniqueness/nonzeroness condition on $z₀$ occur.

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