Separating hyperplane theorem

Proved

ConvexOptimization.separating_hyperplane_disjoint_convex

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

convexanalysisconvexoptimizationlog-concavity

The separating hyperplane theorem.

Let $C$ and $D$ be nonempty convex subsets of $\mathbb{R}^n$ that are disjoint, $C \cap D = \emptyset$ . Then there is a hyperplane separating them: there exist a nonzero vector $a \in \mathbb{R}^n$ and a scalar $b \in \mathbb{R}$ with

\langle a, x\rangle \le b \quad \text{for every } x \in C, \qquad\text{and}\qquad \langle a, x\rangle \ge b \quad \text{for every } x \in D .

The separation is not asserted to be strict — with only convexity and disjointness in hand, the two sets may touch in the limit (as do $\{(x,y) : y \le 0\}$ and $\{(x,y) : x > 0,\ y \le 1/x\}$ ), and strictness requires an additional hypothesis such as compactness of one set and closedness of the other.

This is the geometric foundation of the whole duality theory: strong duality, supporting hyperplanes, theorems of the alternative, and the existence of subgradients are all obtained by separating a suitable pair of convex sets. It is the single most reused statement of Chapter 2.

Formalization Note Vectors live in EuclideanSpace ℝ (Fin n); the conclusion is an existential over a ≠ 0 and b, with the two families of inequalities stated pointwise. Source: B&V §2.5.1, pp. 46–48.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.separating_hyperplane_disjoint_convex {n : ℕ}
    (C D : Set (EuclideanSpace ℝ (Fin n)))
    (hC : Convex ℝ C) (hD : Convex ℝ D)
    (hCne : C.Nonempty) (hDne : D.Nonempty) (hdisj : Disjoint C D) :
    ∃ a : EuclideanSpace ℝ (Fin n), a ≠ 0 ∧ ∃ b : ℝ,
      (∀ x ∈ C, ⟪a, x⟫ ≤ b) ∧ (∀ x ∈ D, b ≤ ⟪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. 46-48, §2.5.1 (separating hyperplane theorem)

Read-back

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

Theorem statement. For every natural number $n$ and every pair of subsets $C, D$ of Euclidean $n$ -space that are convex (over $\mathbb{R}$ ), nonempty, and disjoint ( $C \cap D = \varnothing$ ), there exist a vector $a \in \mathbb{R}^n$ with $a \ne 0$ and a real number $b$ such that $\langle a, x\rangle \le b$ for every $x \in C$ and $b \le \langle a, x\rangle$ for every $x \in D$ . Both separation inequalities are non-strict (weak separation: both sets may touch the hyperplane $\{\langle a, \cdot\rangle = b\}$ , and nothing rules out both lying inside it). No closedness, boundedness, openness, or compactness is assumed of either set. Degenerate case: when $n = 0$ the ambient space is a single point, so two nonempty disjoint subsets cannot exist and the statement is vacuously true there; for $n \ge 1$ the content is the general weak separation of arbitrary disjoint nonempty convex sets in finite dimension.

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