Prove2Me

First-order optimality criterion

Proved
ConvexOptimization.optimal_iff_gradient_variational

by Shuze Chen · Aug 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexoptimizationdualitykkt

The first-order optimality criterion for differentiable convex problems — inequality (4.21) of Boyd & Vandenberghe.

Let X⊆RnX \subseteq \mathbb{R}^n be convex, let f:Rn→Rf : \mathbb{R}^n \to \mathbb{R} be differentiable with gradient field ∇f\nabla f, and assume ff is convex on XX. Then for x∈Xx \in X,

x minimizes f over X⟺⟨∇f(x), y−x⟩≥0for every y∈X.x \text{ minimizes } f \text{ over } X \qquad\Longleftrightarrow\qquad \langle \nabla f(x),\, y - x\rangle \ge 0 \quad \text{for every } y \in X .

Geometrically the condition says that −∇f(x)-\nabla f(x) defines a supporting hyperplane of XX at xx: moving from xx toward any other feasible point cannot decrease ff to first order. For an unconstrained problem (X=RnX = \mathbb{R}^n) it collapses to ∇f(x)=0\nabla f(x) = 0.

This is the bridge between the variational and the algebraic descriptions of optimality, and it is used in both directions in this mission — to convert stationarity of the Lagrangian into optimality of a KKT point, and to characterize Euclidean projection.

Formalization Note The gradient is an explicit field f' with ∀ x, HasGradientAt f (f' x) x, and optimality is IsMinOn f X x. Convexity of the domain is assumed separately as Convex ℝ X alongside ConvexOn ℝ X f. Source: B&V §4.2.3, p. 139, eq. (4.21).

Preamble
import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory
Formal statement
theorem ConvexOptimization.optimal_iff_gradient_variational {n : ℕ}
    (X : Set (EuclideanSpace ℝ (Fin n))) (hX : Convex ℝ X)
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (f' : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf : ∀ x, HasGradientAt f (f' x) x) (hfc : ConvexOn ℝ X f)
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ X) :
    IsMinOn f X x ↔ ∀ y ∈ X, 0 ≤ ⟪f' x, y - x⟫ := by
  sorry
Source
Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 139, §4.2.3 eq. (4.21) (first-order optimality criterion for differentiable convex problems)

View graph