First-order optimality criterion

Proved

ConvexOptimization.optimal_iff_gradient_variational

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

convexoptimizationdualitykkt

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

Let $X \subseteq \mathbb{R}^n$ be convex, let $f : \mathbb{R}^n \to \mathbb{R}$ be differentiable with gradient field $\nabla f$ , and assume $f$ is convex on $X$ . Then for $x \in 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 $-\nabla f(x)$ defines a supporting hyperplane of $X$ at $x$ : moving from $x$ toward any other feasible point cannot decrease $f$ to first order. For an unconstrained problem ( $X = \mathbb{R}^n$ ) it collapses to $\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)

Read-back

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

Theorem. Let $n$ be any natural number (implicit), $X \subseteq \mathbb{R}^n$ , $f : \mathbb{R}^n \to \mathbb{R}$ , and $G : \mathbb{R}^n \to \mathbb{R}^n$ . Assume: (a) $X$ is convex; (b) for every point $x$ of the whole space $\mathbb{R}^n$ (not just points of $X$ ), $f$ has gradient $G(x)$ at $x$ — i.e. $f$ is differentiable at every point of $\mathbb{R}^n$ and $G$ is its gradient field; (c) $f$ is convex on $X$ (which again subsumes convexity of $X$ ); (d) $x \in X$ . Then the following equivalence (a genuine if-and-only-if) holds:

x \text{ minimizes } f \text{ on } X \quad\Longleftrightarrow\quad \forall\, y \in X,\;\; 0 \le \langle G(x),\, y - x\rangle,

where "minimizes" means $f(x) \le f(y)$ for all $y \in X$ (non-strict), and the right-hand side is the variational inequality with the non-strict direction $\langle G(x), y-x\rangle \ge 0$ . Edge cases: if $X$ is empty the hypothesis $x \in X$ is unsatisfiable, so the statement is vacuous there; the differentiability hypothesis is over all of $\mathbb{R}^n$ , which is stronger than differentiability on $X$ alone.

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