Local minima of convex functions are global

Proved

ConvexOptimization.local_min_is_global_min

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

convexoptimizationdualitykkt

A local minimum of a convex function is a global minimum.

Let $X \subseteq \mathbb{R}^n$ and let $f$ be convex on $X$ . Suppose $x \in X$ is a local minimum of $f$ on $X$ : there is a radius $r > 0$ such that

f(x) \le f(y) \qquad \text{for every } y \in X \text{ with } \lVert y - x\rVert_2 < r .

Then $x$ minimizes $f$ over all of $X$ .

This is the structural fact that makes convex optimization tractable: there are no strictly local traps, so any method that certifies local optimality certifies global optimality, and the words "optimal" and "locally optimal" can be used interchangeably throughout the theory. Convexity of $X$ itself is not needed as a separate hypothesis — it is carried by ConvexOn ℝ X f, which asserts convexity of the domain along with the inequality.

Formalization Note The conclusion is Mathlib's IsMinOn f X x; the local hypothesis is stated with an explicit radius rather than with a neighbourhood filter, matching the book's phrasing. Source: B&V §4.2.2, p. 138.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.local_min_is_global_min {n : ℕ}
    (X : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : ConvexOn ℝ X f) (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ X)
    (hloc : ∃ r > 0, ∀ y ∈ X, ‖y - x‖ < r → f x ≤ f y) :
    IsMinOn f X x := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 138, §4.2.2 (any locally optimal point of a convex problem is globally optimal)

Read-back

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

Theorem. Let $n$ be any natural number (implicit; $n = 0$ allowed), $X \subseteq \mathbb{R}^n$ a set, and $f : \mathbb{R}^n \to \mathbb{R}$ a function. Assume: (a) $f$ is convex on $X$ in the standard sense (this hypothesis includes the convexity of the set $X$ itself, together with the convexity inequality for $f$ between points of $X$ ); (b) $x \in X$ ; (c) $x$ is a local minimizer of $f$ relative to $X$ , in the precise form: there exists $r > 0$ (strictly positive) such that for every $y \in X$ with $\|y - x\| < r$ one has $f(x) \le f(y)$ (non-strict). The conclusion is that $x$ is a global minimizer of $f$ on $X$ : $f(x) \le f(y)$ for every $y \in X$ . No continuity or differentiability of $f$ is assumed, $f$ is a total function on all of $\mathbb{R}^n$ (its values outside $X$ are unconstrained), and all minimality statements are non-strict inequalities.

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