Double dual cone = closed conic hull

Proved

ConvexOptimization.dualCone_dualCone_eq_closure_conicHull

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

convexanalysisconvexoptimizationlog-concavity

The double dual cone is the closed conic hull.

For an arbitrary $K \subseteq \mathbb{R}^n$ , write $K^{*} = \{y : \langle x,y\rangle \ge 0 \ \forall x \in K\}$ for the dual cone and $\operatorname{cone}(K)$ for the set of all finite nonnegative combinations of elements of $K$ . Then

K^{**} \;=\; \overline{\operatorname{cone}(K)} .

Dualizing twice is therefore a closure operation, not the identity: it adds exactly the nonnegative combinations of the elements of $K$ and then the limit points. In particular $K^{**} = K$ precisely when $K$ is a closed convex cone, which is the conic analogue of the Fenchel–Moreau theorem for functions.

The identity is what licenses moving between a cone described by generators and the same cone described by inequalities — the two representations of conic constraints used throughout conic and semidefinite programming.

Formalization Note Both dualCone and conicHull are the mission's own definitions, and no hypothesis is placed on K — the theorem holds for every subset, with the closure and the conic hull doing all the work. Source: B&V §2.6.1, p. 53, and exercise 2.31(e), p. 64.

Preamble

import Mathlib
import Definitions.Def_dualCone
import Definitions.Def_conicHull

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.dualCone_dualCone_eq_closure_conicHull {n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin n))) :
    dualCone (dualCone K) = closure (conicHull K) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 53, 64, §2.6.1 (dual cones of dual cones) and exercise 2.31(e)

Read-back

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

Theorem statement. For every natural number $n$ and every subset $K$ of Euclidean $n$ -space — no convexity, closedness, nonemptiness, or cone assumption — the following two sets are equal: (left) the double dual cone $\{\, z \mid \forall y,\ (\forall x \in K,\ 0 \le \langle x, y\rangle) \Rightarrow 0 \le \langle y, z\rangle \,\}$ , where the dual cone of a set $S$ is $\{y \mid \forall x \in S,\ \langle x, y\rangle \ge 0\}$ (nonnegative-inner-product convention); (right) the topological closure, in the Euclidean topology, of the set of all finite nonnegative linear combinations $\sum_{i<m} \theta_i u_i$ with $m \in \mathbb{N}$ , $\theta_i \ge 0$ , $u_i \in K$ (the file's conicHull, which contains $0$ via the empty sum $m = 0$ ). Edge cases quantified over: $K = \varnothing$ , for which the dual cone of $K$ is the whole space and the conic hull is $\{0\}$ ; and $n = 0$ , where every set involved is $\varnothing$ or $\{0\}$ .

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