Convex cones

In a vector space E over ℝ, we define a convex cone as a subset 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 semimodules.

We also 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

Implementation notes

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

References

• https://en.wikipedia.org/wiki/Convex_cone

TODO

• Define the dual cone.

Definition of convex_cone and basic properties

Convex cones with extra properties

Positive cone of an ordered semimodule

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.