Convex cones #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In a 𝕜-module E, we define a convex cone as a set s such that a • x + b • y ∈ s whenever x, y ∈ s and a, b > 0. We prove that convex cones form a complete_lattice, and define their images (convex_cone.map) and preimages (convex_cone.comap) under linear maps.

We define pointed, blunt, flat and salient cones, and prove the correspondence between convex cones and ordered modules.

We define convex.to_cone to be the minimal cone that includes a given convex set.

Main statements #

We prove two extension theorems:

• riesz_extension: M. Riesz extension theorem says that if s is a convex cone in a real vector space E, p is a submodule of E such that p + s = E, and f is a linear function p → ℝ which is nonnegative on p ∩ s, then there exists a globally defined linear function g : E → ℝ that agrees with f on p, and is nonnegative on s.
• exists_extension_of_le_sublinear: Hahn-Banach theorem: if N : E → ℝ is a sublinear map, f is a linear map defined on a subspace of E, and f x ≤ N x for all x in the domain of f, then f can be extended to the whole space to a linear map g such that g x ≤ N x for all x

We prove the following theorems:

• convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem: This variant of the hyperplane separation theorem states that given a nonempty, closed, convex cone K in a complete, real inner product space H and a point b disjoint from it, there is a vector y which separates b from K in the sense that for all points x in K, 0 ≤ ⟪x, y⟫_ℝ and ⟪y, b⟫_ℝ < 0. This is also a geometric interpretation of the Farkas lemma.
• convex_cone.inner_dual_cone_of_inner_dual_cone_eq_self:

Implementation notes #

While convex 𝕜 is a predicate on sets, convex_cone 𝕜 E is a bundled convex cone.

References #

• https://en.wikipedia.org/wiki/Convex_cone
• Stephen P. Boyd and Lieven Vandenberghe, Convex Optimization
• Emo Welzl and Bernd Gärtner, Cone Programming

Definition of convex_cone and basic properties #

Convex cones with extra properties #

Submodules are cones #

Positive cone of an ordered module #

Cone over a convex set #

M. Riesz extension theorem #

Given a convex cone s in a vector space E, a submodule p, and a linear f : p → ℝ, assume that f is nonnegative on p ∩ s and p + s = E. Then there exists a globally defined linear function g : E → ℝ that agrees with f on p, and is nonnegative on s.

We prove this theorem using Zorn's lemma. riesz_extension.step is the main part of the proof. It says that if the domain p of f is not the whole space, then f can be extended to a larger subspace p ⊔ span ℝ {y} without breaking the non-negativity condition.

In riesz_extension.exists_top we use Zorn's lemma to prove that we can extend f to a linear map g on ⊤ : submodule E. Mathematically this is the same as a linear map on E but in Lean ⊤ : submodule E is isomorphic but is not equal to E. In riesz_extension we use this isomorphism to prove the theorem.