Prove2Me

Supporting hyperplane theorem

Proved
ConvexOptimization.supporting_hyperplane

by Shuze Chen · Aug 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexanalysisconvexoptimizationlog-concavity

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

Let C⊆RnC \subseteq \mathbb{R}^n be convex and let x0x_0 be a point of the boundary of CC. Then there is a nonzero a∈Rna \in \mathbb{R}^n with

⟨a,x⟩  ≤  ⟨a,x0⟩for every x∈C.\langle a, x\rangle \;\le\; \langle a, x_0\rangle \qquad \text{for every } x \in C .

The hyperplane {x:⟨a,x⟩=⟨a,x0⟩}\{x : \langle a,x\rangle = \langle a,x_0\rangle\} touches CC at x0x_0 and keeps all of CC 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 ff at (x,f(x))(x, f(x)) is exactly a subgradient of ff at xx — 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)

View graph