No strict linearized descent at a local minimizer

Proved

VectorSpaceOpt.kkt_no_strict_linearized_descent

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

kktlinearizationlocal-minimumstrict-feasibility

Let x₀ be feasible for the cone inequality G x ≤ₚ 0 and a local minimizer of f on that feasible set. Suppose f and G have continuous-linear Gâteaux derivatives f' and G' at x₀. Then there is no direction h that strictly lowers the linearized objective and simultaneously enters the strict interior of the linearized feasible cone:

¬∃h,\; f'h<0 \;∧\; Gx₀+G'h <ₚ 0.

The assertion is deliberately based on IsLocalMinOn, not a stronger global-minimum hypothesis. It is the nonintersection fact that turns local optimality into a geometric separation problem and isolates the only use of the nonlinear maps in the KKT argument.

Preamble

import Definitions.Def_VectorSpaceOpt_cone_optimization

open Set

Formal statement

namespace VectorSpaceOpt

/-- The nonintersection step in Luenberger's proof of §9.4, Theorem 1. -/
theorem kkt_no_strict_linearized_descent
    {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)
    (hf : HasGateauxDerivAt f f' x₀) (hG : HasGateauxDerivAt G G' x₀)
    (hmin : IsLocalMinOn f {x | coneLE P (G x) 0} x₀)
    (hfeas : coneLE P (G x₀) 0) :
    ¬ ∃ h : X, f' h < 0 ∧ coneLT P (G x₀ + G' h) 0 := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 9, §9.4, first part of the proof of Theorem 1, printed p. 250 (physical PDF p. 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$ , $f:X→ℝ$ , $G:X→Z$ , $x₀∈X$ , and $f':X→ℝ$ , $G':X→Z$ continuous real-linear maps. Assume that for every direction $h$ , the line derivatives at $t=0$ of $t↦f(x₀+th)$ and $t↦G(x₀+th)$ are $f'h$ and $G'h$ . Assume $x₀$ is a local minimum of $f$ relative to the cone-feasible set of all $x$ with $-G(x)∈P$ , and separately assume the feasibility condition $-G(x₀)∈P$ . Then there is no $h∈X$ for which both $f'h<0$ and $-(G(x₀)+G'h)∈interior(P)$ . No nonempty-interior or cone-regularity hypothesis is made, so if $interior(P)$ is empty the negated existential conclusion is automatic.

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