# mathlibdocumentation

analysis.convex.cone

# 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 modules.

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

We define set.inner_dual_cone to be the cone consisting of all points y such that for all points x in a given set 0 ≤ ⟪ x, y ⟫.

## 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.