Second-order characterization of convexity

Proved

ConvexOptimization.convexOn_iff_hessian_nonneg

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

convexanalysisconvexoptimizationlog-concavity

Second-order characterization of convexity: a twice differentiable function is convex exactly when its Hessian is positive semidefinite.

Let $\Omega \subseteq \mathbb{R}^n$ be open and convex and let $f$ be twice continuously differentiable on $\Omega$ . Then

f \text{ is convex on } \Omega \qquad\Longleftrightarrow\qquad \langle \nabla^2 f(x)\, v,\, v\rangle \ge 0 \quad \text{for every } x \in \Omega \text{ and every } v \in \mathbb{R}^n,

i.e. $\nabla^2 f(x) \succeq 0$ throughout $\Omega$ .

This is the criterion one actually applies to a concrete function: convexity of a quadratic form reduces to positive semidefiniteness of its matrix, and convexity along every line is exactly nonnegativity of the second derivative of the restriction. Strengthening the right-hand side to $\nabla^2 f(x) \succeq mI$ with $m > 0$ gives strong convexity, the hypothesis under which the convergence rates of later missions are stated.

Formalization Note Smoothness is ContDiffOn ℝ 2 f Ω, and the Hessian appears as the iterated Fréchet derivative fderiv ℝ (fderiv ℝ f) x v v rather than as a matrix, which avoids choosing a basis; openness of Ω is needed for these derivatives to be defined at every point of the domain. Source: B&V §3.1.4, p. 71.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.convexOn_iff_hessian_nonneg {n : ℕ}
    (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩo : IsOpen Ω) (hΩc : Convex ℝ Ω)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : ContDiffOn ℝ 2 f Ω) :
    ConvexOn ℝ Ω f ↔
      ∀ x ∈ Ω, ∀ v : EuclideanSpace ℝ (Fin n),
        0 ≤ fderiv ℝ (fderiv ℝ f) x v v := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 71, §3.1.4 (second-order conditions for convexity)

Read-back

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

Theorem statement. Let $\Omega \subseteq \mathbb{R}^n$ (Euclidean) be open and convex, and let $f : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable on $\Omega$ (ContDiffOn of order $2$ ; nothing is assumed about $f$ off $\Omega$ ). The claim is the equivalence: $f$ is convex on $\Omega$ (Mathlib ConvexOn: $\Omega$ convex — redundant with the hypothesis — together with $f(ax+by) \le a f(x) + b f(y)$ for $x,y \in \Omega$ , $a,b \ge 0$ , $a+b=1$ ) $\iff$ for every $x \in \Omega$ and every direction $v \in \mathbb{R}^n$ , $0 \le D(Df)(x)\,[v][v]$ , where $Df$ denotes the globally defined total Fréchet-derivative function (assigned the junk value $0$ at any point where $f$ is not differentiable) and $D(Df)(x)$ is the Fréchet derivative of that global function at $x$ (again junk $0$ where it fails to exist). Because $\Omega$ is open and $f$ is $C^2$ on it, at points of $\Omega$ these coincide with the genuine first and second derivatives, so the right-hand side is the nonnegativity of the second directional derivative $\partial^2_v f(x)$ — i.e. only the diagonal $(v, v)$ of the second-derivative bilinear form is constrained, for each single direction $v$ (including $v = 0$ , where it is trivially $0 \le 0$ ). If $\Omega = \varnothing$ both sides are vacuous.

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