# mathlibdocumentation

analysis.convex.cone

# Convex cones #

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 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 π E is a bundled convex cone.

## References #

### Definition of convex_cone and basic properties #

structure convex_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [has_scalar π 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.has_coe {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_coe (convex_cone π E) (set E)
Equations
@[protected, instance]
def convex_cone.has_mem {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
(convex_cone π E)
Equations
@[protected, instance]
def convex_cone.has_le {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_le (convex_cone π E)
Equations
@[protected, instance]
def convex_cone.has_lt {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_lt (convex_cone π E)
Equations
@[simp, norm_cast]
theorem convex_cone.mem_coe {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) {x : E} :
@[simp]
theorem convex_cone.mem_mk {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π 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
theorem convex_cone.ext' {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {S T : convex_cone π E} (h : βS = βT) :
S = T

Two convex_cones are equal if the underlying sets are equal.

@[protected]
theorem convex_cone.ext'_iff {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {S T : convex_cone π E} :

Two convex_cones are equal if and only if the underlying sets are equal.

@[ext]
theorem convex_cone.ext {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {S T : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) {c : π} {x : E} (hc : 0 < c) (hx : x β S) :
theorem convex_cone.add_mem {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) β¦x : Eβ¦ (hx : x β S) β¦y : Eβ¦ (hy : y β S) :
x + y β S
@[protected, instance]
def convex_cone.has_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_inf (convex_cone π E)
Equations
theorem convex_cone.coe_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S T : convex_cone π E) :
theorem convex_cone.mem_inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S T : convex_cone π E) {x : E} :
@[protected, instance]
def convex_cone.has_Inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_Inf (convex_cone π E)
Equations
theorem convex_cone.mem_Inf {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {x : E} {S : set (convex_cone π E)} :
β β (s : convex_cone π E), s β S β x β s
@[protected, instance]
def convex_cone.has_bot (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_bot (convex_cone π E)
Equations
theorem convex_cone.mem_bot (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] (x : E) :
@[protected, instance]
def convex_cone.has_top (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
has_top (convex_cone π E)
Equations
theorem convex_cone.mem_top (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] (x : E) :
@[protected, instance]
def convex_cone.complete_lattice (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
Equations
@[protected, instance]
def convex_cone.inhabited (π : Type u_1) {E : Type u_2} [ordered_semiring π] [has_scalar π E] :
inhabited (convex_cone π E)
Equations
@[protected]
theorem convex_cone.convex {π : Type u_1} {E : Type u_2} [ordered_semiring π] [module π E] (S : convex_cone π E) :
convex π βS
theorem convex_cone.smul_mem_iff {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [mul_action π E] (S : convex_cone π E) {c : π} (hc : 0 < c) {x : E} :
def convex_cone.map {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] (f : E ββ[π] F) (S : convex_cone π E) :
convex_cone π F

The image of a convex cone under a π-linear map is a convex cone.

Equations
theorem convex_cone.map_map {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [linear_ordered_field π] [module π E] [module π F] [module π G] (g : F ββ[π] G) (f : E ββ[π] F) (S : convex_cone π E) :
S) = convex_cone.map (g.comp f) S
@[simp]
theorem convex_cone.map_id {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π E) :
def convex_cone.comap {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] (f : E ββ[π] F) (S : convex_cone π F) :
convex_cone π E

The preimage of a convex cone under a π-linear map is a convex cone.

Equations
@[simp]
theorem convex_cone.comap_id {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π E) :
theorem convex_cone.comap_comap {π : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [linear_ordered_field π] [module π E] [module π F] [module π G] (g : F ββ[π] G) (f : E ββ[π] F) (S : convex_cone π G) :
@[simp]
theorem convex_cone.mem_comap {π : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π] [module π E] [module π F] {f : E ββ[π] F} {S : convex_cone π F} {x : E} :
theorem convex_cone.to_ordered_smul {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (S : convex_cone π E) (h : β (x y : E), x β€ y β y - x β S) :
ordered_smul π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) :
Prop

A convex cone is pointed if it includes 0.

Equations
def convex_cone.blunt {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) :
theorem convex_cone.blunt_iff_not_pointed {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) :
def convex_cone.flat {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) :
theorem convex_cone.flat.pointed {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {S : convex_cone π E} (hS : S.flat) :

A flat cone is always pointed (contains 0).

theorem convex_cone.blunt.salient {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] {S : convex_cone π E} :
S.blunt β S.salient

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

def convex_cone.to_preorder {π : Type u_1} {E : Type u_2} [ordered_semiring π] [has_scalar π E] (S : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π 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} [ordered_semiring π] [has_scalar π E] (S : convex_cone π E) (hβ : S.pointed) (hβ : S.salient) :

A pointed and salient cone defines an ordered_add_comm_group.

Equations

### Positive cone of an ordered module #

def convex_cone.positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :
convex_cone π E

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

Equations
theorem convex_cone.salient_positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :

The positive cone of an ordered module is always salient.

theorem convex_cone.pointed_positive_cone (π : Type u_1) (E : Type u_2) [ordered_semiring π] [module π E] [ordered_smul π E] :

The positive cone of an ordered module is always pointed.

### Cone over a convex set #

def convex.to_cone {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) (hs : convex π s) :
convex_cone π 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} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π 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} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) {x : E} :
x β hs β β (c : π), 0 < c β§ c β’ x β s
theorem convex.subset_to_cone {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) :
theorem convex.to_cone_is_least {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) :
is_least {t : convex_cone π 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} [linear_ordered_field π] [module π E] {s : set E} (hs : convex π s) :
hs = has_Inf.Inf {t : convex_cone π E | s β βt}
theorem convex_hull_to_cone_is_least {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) :
is_least {t : convex_cone π E | s β βt} (convex.to_cone (β(convex_hull π) s) _)
theorem convex_hull_to_cone_eq_Inf {π : Type u_1} {E : Type u_2} [linear_ordered_field π] [module π E] (s : set E) :
convex.to_cone (β(convex_hull π) s) _ = has_Inf.Inf {t : convex_cone π 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 : β) (nonneg : β (x : β₯(f.domain)), βx β s β 0 β€ βf x) (dense : β (y : E), β (x : β₯(f.domain)), βx + y β s) (hdom : f.domain β  β€) :
β (g : , 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 : β) (hp_nonneg : β (x : β₯(p.domain)), βx β s β 0 β€ βp x) (hp_dense : β (y : E), β (x : β₯(p.domain)), βx + y β s) :
β (q : (H : q β₯ p), β§ β (x : β₯(q.domain)), βx β s β 0 β€ βq x
theorem riesz_extension {E : Type u_2} [ E] (s : E) (f : β) (nonneg : β (x : β₯(f.domain)), βx β s β 0 β€ βf x) (dense : β (y : E), β (x : β₯(f.domain)), βx + y β s) :
β (g : , (β (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 : β) (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 : , (β (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.

### The dual cone #

def set.inner_dual_cone {H : Type u_5} (s : set H) :

The dual cone is the cone consisting of all points y such that for all points x in a given set 0 β€ βͺ x, y β«.

Equations
theorem mem_inner_dual_cone {H : Type u_5} (y : H) (s : set H) :
β β (x : H), x β s β 0 β€
@[simp]
theorem inner_dual_cone_empty {H : Type u_5}  :
theorem inner_dual_cone_le_inner_dual_cone {H : Type u_5} (s t : set H) (h : t β s) :
theorem pointed_inner_dual_cone {H : Type u_5} (s : set H) :