# mathlib3documentation

analysis.convex.cone.basic

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

### Definition of convex_cone and basic properties #

structure convex_cone (𝕜 : Type u_1) (E : Type u_2) [ E] :
Type u_2

A convex cone is a subset s of a 𝕜-module such that a • x + b • y ∈ s whenever a, b > 0 and x, y ∈ s.

Instances for convex_cone
@[protected, instance]
def convex_cone.set_like {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[simp]
theorem convex_cone.coe_mk {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {h₁ : ⦃c : 𝕜⦄, 0 < c ⦃x : E⦄, x s c x s} {h₂ : ⦃x : E⦄, x s ⦃y : E⦄, y s x + y s} :
{carrier := s, smul_mem' := h₁, add_mem' := h₂} = s
@[simp]
theorem convex_cone.mem_mk {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {h₁ : ⦃c : 𝕜⦄, 0 < c ⦃x : E⦄, x s c x s} {h₂ : ⦃x : E⦄, x s ⦃y : E⦄, y s x + y s} {x : E} :
x {carrier := s, smul_mem' := h₁, add_mem' := h₂} x s
@[ext]
theorem convex_cone.ext {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} (h : (x : E), x S x T) :
S = T

Two convex_cones are equal if they have the same elements.

theorem convex_cone.smul_mem {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) {c : 𝕜} {x : E} (hc : 0 < c) (hx : x S) :
c x S
theorem convex_cone.add_mem {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) ⦃x : E⦄ (hx : x S) ⦃y : E⦄ (hy : y S) :
x + y S
@[protected, instance]
def convex_cone.add_mem_class {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[protected, instance]
def convex_cone.has_inf {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[simp]
theorem convex_cone.coe_inf {𝕜 : Type u_1} {E : Type u_2} [ E] (S T : E) :
(S T) = S T
theorem convex_cone.mem_inf {𝕜 : Type u_1} {E : Type u_2} [ E] (S T : E) {x : E} :
x S T x S x T
@[protected, instance]
def convex_cone.has_Inf {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[simp]
theorem convex_cone.coe_Inf {𝕜 : Type u_1} {E : Type u_2} [ E] (S : set E)) :
(has_Inf.Inf S) = (s : E) (H : s S), s
theorem convex_cone.mem_Inf {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {S : set E)} :
x (s : E), s S x s
@[simp]
theorem convex_cone.coe_infi {𝕜 : Type u_1} {E : Type u_2} [ E] {ι : Sort u_3} (f : ι E) :
(infi f) = (i : ι), (f i)
theorem convex_cone.mem_infi {𝕜 : Type u_1} {E : Type u_2} [ E] {ι : Sort u_3} {x : E} {f : ι E} :
x infi f (i : ι), x f i
@[protected, instance]
def convex_cone.has_bot (𝕜 : Type u_1) {E : Type u_2} [ E] :
Equations
theorem convex_cone.mem_bot (𝕜 : Type u_1) {E : Type u_2} [ E] (x : E) :
@[simp]
theorem convex_cone.coe_bot (𝕜 : Type u_1) {E : Type u_2} [ E] :
@[protected, instance]
def convex_cone.has_top (𝕜 : Type u_1) {E : Type u_2} [ E] :
Equations
theorem convex_cone.mem_top (𝕜 : Type u_1) {E : Type u_2} [ E] (x : E) :
@[simp]
theorem convex_cone.coe_top (𝕜 : Type u_1) {E : Type u_2} [ E] :
@[protected, instance]
def convex_cone.complete_lattice (𝕜 : Type u_1) {E : Type u_2} [ E] :
Equations
@[protected, instance]
def convex_cone.inhabited (𝕜 : Type u_1) {E : Type u_2} [ E] :
Equations
@[protected]
theorem convex_cone.convex {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
S
theorem convex_cone.smul_mem_iff {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) {c : 𝕜} (hc : 0 < c) {x : E} :
c x S x S
def convex_cone.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →ₗ[𝕜] F) (S : E) :
F

The image of a convex cone under a 𝕜-linear map is a convex cone.

Equations
@[simp]
theorem convex_cone.mem_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E →ₗ[𝕜] F} {S : E} {y : F} :
y (x : E) (H : x S), f x = y
theorem convex_cone.map_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : E) :
S) = convex_cone.map (g.comp f) S
@[simp]
theorem convex_cone.map_id {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
def convex_cone.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →ₗ[𝕜] F) (S : F) :
E

The preimage of a convex cone under a 𝕜-linear map is a convex cone.

Equations
@[simp]
theorem convex_cone.coe_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] (f : E →ₗ[𝕜] F) (S : F) :
@[simp]
theorem convex_cone.comap_id {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
theorem convex_cone.comap_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [ E] [ F] [ G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : G) :
@[simp]
theorem convex_cone.mem_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [ E] [ F] {f : E →ₗ[𝕜] F} {S : F} {x : E} :
x f x S
theorem convex_cone.to_ordered_smul {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) (h : (x y : E), x y y - x S) :
E

Constructs an ordered module given an ordered_add_comm_group, a cone, and a proof that the order relation is the one defined by the cone.

### Convex cones with extra properties #

def convex_cone.pointed {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
Prop

A convex cone is pointed if it includes 0.

Equations
def convex_cone.blunt {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
Prop

A convex cone is blunt if it doesn't include 0.

Equations
theorem convex_cone.pointed_iff_not_blunt {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
theorem convex_cone.blunt_iff_not_pointed {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
theorem convex_cone.pointed.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} (h : S T) :
theorem convex_cone.blunt.anti {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} (h : T S) :
def convex_cone.flat {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
Prop

A convex cone is flat if it contains some nonzero vector x and its opposite -x.

Equations
def convex_cone.salient {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
Prop

A convex cone is salient if it doesn't include x and -x for any nonzero x.

Equations
theorem convex_cone.salient_iff_not_flat {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
theorem convex_cone.flat.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} (h : S T) :
theorem convex_cone.salient.anti {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} (h : T S) :
theorem convex_cone.flat.pointed {𝕜 : Type u_1} {E : Type u_2} [ E] {S : E} (hS : S.flat) :

A flat cone is always pointed (contains 0).

theorem convex_cone.blunt.salient {𝕜 : Type u_1} {E : Type u_2} [ E] {S : E} :

A blunt cone (one not containing 0) is always salient.

def convex_cone.to_preorder {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) (h₁ : S.pointed) :

A pointed convex cone defines a preorder.

Equations
def convex_cone.to_partial_order {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) (h₁ : S.pointed) (h₂ : S.salient) :

A pointed and salient cone defines a partial order.

Equations
def convex_cone.to_ordered_add_comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) (h₁ : S.pointed) (h₂ : S.salient) :

A pointed and salient cone defines an ordered_add_comm_group.

Equations
@[protected, instance]
def convex_cone.has_zero {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[simp]
theorem convex_cone.mem_zero {𝕜 : Type u_1} {E : Type u_2} [ E] (x : E) :
x 0 x = 0
@[simp]
theorem convex_cone.coe_zero {𝕜 : Type u_1} {E : Type u_2} [ E] :
0 = 0
theorem convex_cone.pointed_zero {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[protected, instance]
def convex_cone.has_add {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[simp]
theorem convex_cone.mem_add {𝕜 : Type u_1} {E : Type u_2} [ E] {K₁ K₂ : E} {a : E} :
a K₁ + K₂ (x y : E), x K₁ y K₂ x + y = a
@[protected, instance]
def convex_cone.add_zero_class {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations
@[protected, instance]
def convex_cone.add_comm_semigroup {𝕜 : Type u_1} {E : Type u_2} [ E] :
Equations

### Submodules are cones #

def submodule.to_convex_cone {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
E

Every submodule is trivially a convex cone.

Equations
@[simp]
theorem submodule.coe_to_convex_cone {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :
@[simp]
theorem submodule.mem_to_convex_cone {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {S : E} :
x S
@[simp]
theorem submodule.to_convex_cone_le_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {S T : E} :
S T
@[simp]
theorem submodule.to_convex_cone_bot {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[simp]
theorem submodule.to_convex_cone_top {𝕜 : Type u_1} {E : Type u_2} [ E] :
@[simp]
theorem submodule.to_convex_cone_inf {𝕜 : Type u_1} {E : Type u_2} [ E] (S T : E) :
@[simp]
theorem submodule.pointed_to_convex_cone {𝕜 : Type u_1} {E : Type u_2} [ E] (S : E) :

### Positive cone of an ordered module #

def convex_cone.positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
E

The positive cone is the convex cone formed by the set of nonnegative elements in an ordered module.

Equations
@[simp]
theorem convex_cone.mem_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] {x : E} :
0 x
@[simp]
theorem convex_cone.coe_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
E) =
theorem convex_cone.salient_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :

The positive cone of an ordered module is always salient.

theorem convex_cone.pointed_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :

The positive cone of an ordered module is always pointed.

def convex_cone.strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
E

The cone of strictly positive elements.

Note that this naming diverges from the mathlib convention of pos and nonneg due to "positive cone" (convex_cone.positive) being established terminology for the non-negative elements.

Equations
@[simp]
theorem convex_cone.mem_strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] {x : E} :
0 < x
@[simp]
theorem convex_cone.coe_strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
theorem convex_cone.positive_le_strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
theorem convex_cone.salient_strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :

The strictly positive cone of an ordered module is always salient.

theorem convex_cone.blunt_strictly_positive (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :

The strictly positive cone of an ordered module is always blunt.

### Cone over a convex set #

def convex.to_cone {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) (hs : s) :
E

The set of vectors proportional to those in a convex set forms a convex cone.

Equations
theorem convex.mem_to_cone {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : s) {x : E} :
x hs (c : 𝕜), 0 < c (y : E) (H : y s), c y = x
theorem convex.mem_to_cone' {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : s) {x : E} :
x hs (c : 𝕜), 0 < c c x s
theorem convex.subset_to_cone {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : s) :
s hs)
theorem convex.to_cone_is_least {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : s) :
is_least {t : E | s t} hs)

hs.to_cone s is the least cone that includes s.

theorem convex.to_cone_eq_Inf {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : s) :
hs = has_Inf.Inf {t : E | s t}
theorem convex_hull_to_cone_is_least {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) :
is_least {t : E | s t} (convex.to_cone ((convex_hull 𝕜) s) _)
theorem convex_hull_to_cone_eq_Inf {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) :
convex.to_cone ((convex_hull 𝕜) s) _ = has_Inf.Inf {t : E | s t}

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

theorem riesz_extension.step {E : Type u_2} [ E] (s : E) (f : E →ₗ.[] ) (nonneg : (x : (f.domain)), x s 0 f x) (dense : (y : E), (x : (f.domain)), x + y s) (hdom : f.domain ) :
(g : E →ₗ.[] ), f < g (x : (g.domain)), x s 0 g x

Induction step in M. Riesz extension theorem. Given a convex cone s in a vector space E, a partially defined linear map f : f.domain → ℝ, assume that f is nonnegative on f.domain ∩ p and p + s = E. If f is not defined on the whole E, then we can extend it to a larger submodule without breaking the non-negativity condition.

theorem riesz_extension.exists_top {E : Type u_2} [ E] (s : E) (p : E →ₗ.[] ) (hp_nonneg : (x : (p.domain)), x s 0 p x) (hp_dense : (y : E), (x : (p.domain)), x + y s) :
(q : E →ₗ.[] ) (H : q p), q.domain = (x : (q.domain)), x s 0 q x
theorem riesz_extension {E : Type u_2} [ E] (s : E) (f : E →ₗ.[] ) (nonneg : (x : (f.domain)), x s 0 f x) (dense : (y : E), (x : (f.domain)), x + y s) :
(g : E →ₗ[] ), ( (x : (f.domain)), g x = f x) (x : E), x s 0 g x

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.

theorem exists_extension_of_le_sublinear {E : Type u_2} [ E] (f : E →ₗ.[] ) (N : E ) (N_hom : (c : ), 0 < c (x : E), N (c x) = c * N x) (N_add : (x y : E), N (x + y) N x + N y) (hf : (x : (f.domain)), f x N x) :
(g : E →ₗ[] ), ( (x : (f.domain)), g x = f x) (x : E), g x N x

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.