Supporting hyperplane theorem

Proved

ConvexOptimization.supporting_hyperplane

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

convexanalysisconvexoptimizationlog-concavity

The supporting hyperplane theorem: every boundary point of a convex set admits a supporting hyperplane.

Let $C \subseteq \mathbb{R}^n$ be convex and let $x_0$ be a point of the boundary of $C$ . Then there is a nonzero $a \in \mathbb{R}^n$ with

\langle a, x\rangle \;\le\; \langle a, x_0\rangle \qquad \text{for every } x \in C .

The hyperplane $\{x : \langle a,x\rangle = \langle a,x_0\rangle\}$ touches $C$ at $x_0$ and keeps all of $C$ on one side. There is no uniqueness claim: at a corner of a polytope infinitely many supporting hyperplanes exist.

Supporting hyperplanes are the geometric form of the subgradient — a supporting hyperplane to the epigraph of $f$ at $(x, f(x))$ is exactly a subgradient of $f$ at $x$ — and they are the mechanism by which a convex set is recovered as the intersection of the halfspaces containing it, which is the converse direction of the separation theory.

Formalization Note Boundary membership is x₀ ∈ frontier C; no closedness hypothesis on C is needed, since a frontier point of C need not belong to C, and the conclusion is stated for points of C only. Source: B&V §2.5.2, p. 51.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.supporting_hyperplane {n : ℕ}
    (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C)
    (x₀ : EuclideanSpace ℝ (Fin n)) (hx₀ : x₀ ∈ frontier C) :
    ∃ a : EuclideanSpace ℝ (Fin n), a ≠ 0 ∧ ∀ x ∈ C, ⟪a, x⟫ ≤ ⟪a, x₀⟫ := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 51, §2.5.2 (supporting hyperplane theorem)

Read-back

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

Theorem statement. For every $n$ , every convex subset $C$ of Euclidean $n$ -space (nonemptiness is not assumed), and every point $x_0$ in the topological frontier of $C$ (frontier = closure minus interior, for the Euclidean topology), there exists $a \in \mathbb{R}^n$ with $a \ne 0$ such that $\langle a, x\rangle \le \langle a, x_0\rangle$ for every $x \in C$ — i.e. the linear functional $\langle a, \cdot\rangle$ attains at $x_0$ an upper bound for its values on $C$ (non-strict; $C$ may meet the hyperplane). Note $x_0$ is a frontier point, which need not belong to $C$ (it lies in $\overline{C}$ ). Degenerate instances silently included: if $C = \varnothing$ or $C$ is the whole space, or $n = 0$ (one-point space, every subset clopen), the frontier is empty and the statement is vacuous; if $C$ has empty interior (e.g. contained in a proper affine subspace), the frontier equals the whole closure, so the claim then asserts a supporting vector at every point of $\overline{C}$ .

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