First-order characterization of convexity

Proved

ConvexOptimization.convexOn_iff_gradient_inequality

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

convexanalysisconvexoptimizationlog-concavity

First-order characterization of convexity: a differentiable function is convex exactly when its tangent planes lie below its graph.

Let $\Omega \subseteq \mathbb{R}^n$ be open and convex, and let $f$ be differentiable on $\Omega$ with gradient field $\nabla f$ . Then

f \text{ is convex on } \Omega \qquad\Longleftrightarrow\qquad f(y) \;\ge\; f(x) + \langle \nabla f(x),\, y - x\rangle \quad \text{for all } x, y \in \Omega .

The right-hand condition says that the first-order Taylor approximation at any point is a global underestimator of $f$ on $\Omega$ — a remarkable amount of global information extracted from a derivative at a single point.

This is the workhorse of the theory: it yields the first-order optimality criterion, the definition of the subgradient in the nondifferentiable case, and the strong-convexity inequality $f(y) \ge f(x) + \langle\nabla f(x), y-x\rangle + \tfrac{m}{2}\lVert y-x\rVert^2$ that drives all convergence-rate analysis.

Formalization Note The gradient is an explicit field f' tied to f by ∀ x ∈ Ω, HasGradientAt f (f' x) x; openness of Ω is assumed so that the derivative is a genuine (two-sided) gradient at every point of the domain, and convexity of Ω is assumed separately from ConvexOn ℝ Ω f. Source: B&V §3.1.3, pp. 69–70.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.convexOn_iff_gradient_inequality {n : ℕ}
    (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩo : IsOpen Ω) (hΩc : Convex ℝ Ω)
    (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (f' : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf : ∀ x ∈ Ω, HasGradientAt f (f' x) x) :
    ConvexOn ℝ Ω f ↔ ∀ x ∈ Ω, ∀ y ∈ Ω, f x + ⟪f' x, y - x⟫ ≤ f y := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 69-70, §3.1.3 eq. (3.2) (first-order condition for convexity)

Read-back

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

Theorem statement. Let $\Omega$ be a subset of Euclidean $n$ -space that is open and convex, let $f : \mathbb{R}^n \to \mathbb{R}$ be a total function, and let $f' : \mathbb{R}^n \to \mathbb{R}^n$ be a total map such that for every $x \in \Omega$ , $f$ has gradient $f'(x)$ at $x$ — i.e. $f$ is Fréchet-differentiable at $x$ with derivative the linear map $z \mapsto \langle f'(x), z\rangle$ (values of $f'$ outside $\Omega$ are unconstrained and unused). Then the claim is an equivalence: $f$ is convex on $\Omega$ $\iff$ for all $x \in \Omega$ and $y \in \Omega$ , $f(x) + \langle f'(x),\, y - x\rangle \le f(y)$ . "Convex on $\Omega$ " is Mathlib's ConvexOn: the conjunction of ( $\Omega$ convex — already a hypothesis, so this conjunct is redundant on the left) and the Jensen inequality $f(a x + b y) \le a f(x) + b f(y)$ for all $x, y \in \Omega$ and $a, b \ge 0$ with $a + b = 1$ . Only the values of $f$ on $\Omega$ are constrained by either side. Degenerate case: if $\Omega = \varnothing$ (or a singleton is impossible here since $\Omega$ open, but $\Omega=\varnothing$ is allowed) both sides hold vacuously and the equivalence is trivially true.

Human review

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

View graph