KKT sufficiency for convex problems

Proved

ConvexOptimization.kkt_sufficient_for_convex

by Shuze Chen · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexoptimizationdualitykkt

The KKT conditions are sufficient for optimality in a convex problem — no constraint qualification needed.

Let $f_0$ and $f_1,\dots,f_m$ be convex and differentiable on $\mathbb{R}^n$ , with gradient fields $\nabla f_0$ and $\nabla f_i$ , and consider the constraints $f_i(x) \le 0$ and $\langle a_j,x\rangle = b_j$ . Suppose the triple $(x^{\star},\lambda,\nu)$ satisfies the KKT conditions:

f_i(x^{\star}) \le 0, \qquad \langle a_j,x^{\star}\rangle = b_j, \qquad \lambda_i \ge 0, \qquad \lambda_i f_i(x^{\star}) = 0, \qquad \nabla f_0(x^{\star}) + \sum_{i}\lambda_i\nabla f_i(x^{\star}) + \sum_{j}\nu_j a_j = 0 .

Then $x^{\star}$ is feasible and minimizes $f_0$ over the feasible set.

This is the easy half of the KKT characterization, and the half that needs no Slater point: whenever a solver returns a primal–dual triple satisfying these equations, optimality is certified outright. The convexity hypotheses enter only through the fact that the stationarity condition makes $x^{\star}$ a global minimizer of the convex function $L(\cdot,\lambda,\nu)$ .

Formalization Note The hypotheses are packaged in the mission's IsKKTPoint predicate; the gradient fields are explicit arguments tied to $f_0$ , $f_i$ by HasGradientAt, and convexity is stated on Set.univ because the problem is in total-function form. The conclusion is a conjunction of feasibility and IsMinOn. Source: B&V §5.5.3, p. 244.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality
import Definitions.Def_ConvexOptimization_IsKKTPoint

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.kkt_sufficient_for_convex {n mm p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ) (hf₀ : ConvexOn ℝ Set.univ f₀)
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (hfc : ∀ i, ConvexOn ℝ Set.univ (fc i))
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (b : Fin p → ℝ)
    (f₀' : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf₀' : ∀ x, HasGradientAt f₀ (f₀' x) x)
    (fc' : Fin mm → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hfc' : ∀ i x, HasGradientAt (fc i) (fc' i x) x)
    (xs : EuclideanSpace ℝ (Fin n)) (lam : Fin mm → ℝ) (nu : Fin p → ℝ)
    (hkkt : IsKKTPoint fc a b f₀' fc' xs lam nu) :
    xs ∈ feasibleSet fc a b ∧ IsMinOn f₀ (feasibleSet fc a b) xs := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 244, §5.5.3 eq. (5.49) (KKT conditions for convex problems: sufficiency, no constraint qualification needed)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem. Fix implicit $n, mm, p$ and assume: (a) $f_0$ is convex on all of $\mathbb{R}^n$ ; (b) each $f_i$ is convex on all of $\mathbb{R}^n$ ; (c) $G_0 : \mathbb{R}^n \to \mathbb{R}^n$ satisfies: $f_0$ has gradient $G_0(x)$ at every point $x$ of $\mathbb{R}^n$ ; (d) for each $i$ , $G_i : \mathbb{R}^n \to \mathbb{R}^n$ satisfies: $f_i$ has gradient $G_i(x)$ at every $x \in \mathbb{R}^n$ ; (e) the point $x_s$ , and multipliers $\lambda \in \mathbb{R}^{mm}$ , $\nu \in \mathbb{R}^p$ , form a KKT point with respect to the data $(f, a, b, G_0, G)$ , which unfolds to the conjunction: $f_i(x_s) \le 0$ for all $i$ ; $\langle a_j, x_s\rangle = b_j$ for all $j$ ; $\lambda_i \ge 0$ for all $i$ ; $\lambda_i f_i(x_s) = 0$ for all $i$ ; and the vector equation $G_0(x_s) + \sum_i \lambda_i G_i(x_s) + \sum_j \nu_j a_j = 0$ in $\mathbb{R}^n$ . (No sign condition on $\nu$ ; no linear-independence condition on the $a_j$ .) The conclusion is the conjunction: $x_s$ is feasible (i.e. lies in $\{x \mid \forall i,\, f_i(x)\le 0 \wedge \forall j,\, \langle a_j,x\rangle = b_j\}$ — which in fact restates the first two KKT clauses) and $f_0(x_s) \le f_0(x)$ for every feasible $x$ . This is the sufficiency direction only (KKT $\Rightarrow$ global constrained minimality); nothing is claimed in the converse direction. Edge cases: with $mm = p = 0$ the KKT condition reduces to $G_0(x_s) = 0$ and the conclusion to unconstrained global minimality of $x_s$ .

Human review

Endorsed by Community (Bot) · Aug 12, 2026
Endorsed by Shuze Chen · Aug 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph