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

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

A convex cone is a subset s of a vector space over ℝ such that a • x + b • y ∈ s whenever a, b > 0 and x, y ∈ s.

@[instance]
def convex_cone.set.has_coe {E : Type u_1} [ E] :
(set E)

Equations
@[instance]
def convex_cone.has_mem {E : Type u_1} [ E] :

Equations
@[instance]
def convex_cone.has_le {E : Type u_1} [ E] :

Equations
@[instance]
def convex_cone.has_lt {E : Type u_1} [ E] :

Equations
@[simp]
theorem convex_cone.mem_coe {E : Type u_1} [ E] (S : convex_cone E) {x : E} :
x S x S

@[simp]
theorem convex_cone.mem_mk {E : Type u_1} [ E] {s : set E} {h₁ : ∀ ⦃c : ⦄, 0 < c∀ ⦃x : E⦄, x sc x s} {h₂ : ∀ ⦃x : E⦄, x s∀ ⦃y : E⦄, y sx + y s} {x : E} :
x {carrier := s, smul_mem' := h₁, add_mem' := h₂} x s

theorem convex_cone.ext' {E : Type u_1} [ E] {S T : convex_cone E} :
S = TS = T

Two convex_cones are equal if the underlying subsets are equal.

theorem convex_cone.ext'_iff {E : Type u_1} [ E] {S T : convex_cone E} :
S = T S = T

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

@[ext]
theorem convex_cone.ext {E : Type u_1} [ E] {S T : convex_cone E} :
(∀ (x : E), x S x T)S = T

Two convex_cones are equal if they have the same elements.

theorem convex_cone.smul_mem {E : Type u_1} [ E] (S : convex_cone E) {c : } {x : E} :
0 < cx Sc x S

theorem convex_cone.add_mem {E : Type u_1} [ E] (S : convex_cone E) ⦃x : E⦄ (hx : x S) ⦃y : E⦄ :
y Sx + y S

theorem convex_cone.smul_mem_iff {E : Type u_1} [ E] (S : convex_cone E) {c : } (hc : 0 < c) {x : E} :
c x S x S

theorem convex_cone.convex {E : Type u_1} [ E] (S : convex_cone E) :

@[instance]
def convex_cone.has_inf {E : Type u_1} [ E] :

Equations
theorem convex_cone.coe_inf {E : Type u_1} [ E] (S T : convex_cone E) :
(S T) = S T

theorem convex_cone.mem_inf {E : Type u_1} [ E] (S T : convex_cone E) {x : E} :
x S T x S x T

@[instance]
def convex_cone.has_Inf {E : Type u_1} [ E] :

Equations
theorem convex_cone.mem_Inf {E : Type u_1} [ E] {x : E} {S : set (convex_cone E)} :
x Inf S ∀ (s : , s Sx s

@[instance]
def convex_cone.has_bot {E : Type u_1} [ E] :

Equations
theorem convex_cone.mem_bot {E : Type u_1} [ E] (x : E) :

@[instance]
def convex_cone.has_top {E : Type u_1} [ E] :

Equations
theorem convex_cone.mem_top {E : Type u_1} [ E] (x : E) :

@[instance]
def convex_cone.complete_lattice {E : Type u_1} [ E] :

Equations
@[instance]
def convex_cone.inhabited {E : Type u_1} [ E] :

Equations
def convex_cone.map {E : Type u_1} [ E] {F : Type u_2} [ F] :
(E →ₗ[] F)

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

Equations
theorem convex_cone.map_map {E : Type u_1} [ E] {F : Type u_2} [ F] {G : Type u_3} [ 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 {E : Type u_1} [ E] (S : convex_cone E) :

def convex_cone.comap {E : Type u_1} [ E] {F : Type u_2} [ F] :
(E →ₗ[] F)

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

Equations
@[simp]
theorem convex_cone.comap_id {E : Type u_1} [ E] (S : convex_cone E) :

theorem convex_cone.comap_comap {E : Type u_1} [ E] {F : Type u_2} [ F] {G : Type u_3} [ G] (g : F →ₗ[] G) (f : E →ₗ[] F) (S : convex_cone G) :

@[simp]
theorem convex_cone.mem_comap {E : Type u_1} [ E] {F : Type u_2} [ F] {f : E →ₗ[] F} {S : convex_cone F} {x : E} :
x f x S

theorem convex_cone.to_ordered_semimodule {M : Type u_1} [ M] (S : convex_cone M) :
(∀ (x y : M), x y y - x S)

Constructs an ordered semimodule 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 {E : Type u_1} [ E] :
→ Prop

A convex cone is pointed if it includes 0.

Equations
def convex_cone.blunt {E : Type u_1} [ E] :
→ Prop

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

Equations
def convex_cone.flat {E : Type u_1} [ E] :
→ Prop

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

Equations
def convex_cone.salient {E : Type u_1} [ E] :
→ Prop

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

Equations
theorem convex_cone.pointed_iff_not_blunt {E : Type u_1} [ E] (S : convex_cone E) :

theorem convex_cone.salient_iff_not_flat {E : Type u_1} [ E] (S : convex_cone E) :

theorem convex_cone.salient_of_blunt {E : Type u_1} [ E] (S : convex_cone E) :
S.blunt → S.salient

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

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

A pointed convex cone defines a preorder.

Equations
def convex_cone.to_partial_order {E : Type u_1} [ E] (S : convex_cone E) :
S.pointedS.salient

A pointed and salient cone defines a partial order.

Equations
def convex_cone.to_ordered_add_comm_group {E : Type u_1} [ E] (S : convex_cone E) :
S.pointed

A pointed and salient cone defines an ordered_add_comm_group.

Equations

Positive cone of an ordered semimodule

def convex_cone.positive_cone (M : Type u_4) [ M]  :

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

Equations
theorem convex_cone.salient_of_positive_cone (M : Type u_4) [ M]  :

The positive cone of an ordered semimodule is always salient.

theorem convex_cone.pointed_of_positive_cone (M : Type u_4) [ M]  :

The positive cone of an ordered semimodule is always pointed.

Cone over a convex set

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

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

Equations
theorem convex.mem_to_cone {E : Type u_1} [ E] {s : set E} (hs : convex s) {x : E} :
x hs ∃ (c : ) (H : c > 0) (y : E) (H : y s), c y = x

theorem convex.mem_to_cone' {E : Type u_1} [ E] {s : set E} (hs : convex s) {x : E} :
x hs ∃ (c : ) (H : c > 0), c x s

theorem convex.subset_to_cone {E : Type u_1} [ E] {s : set E} (hs : convex s) :
s hs)

theorem convex.to_cone_is_least {E : Type u_1} [ E] {s : set E} (hs : convex s) :
is_least {t : | s t} hs)

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

theorem convex.to_cone_eq_Inf {E : Type u_1} [ E] {s : set E} (hs : convex s) :
hs = Inf {t : | s t}

theorem convex_hull_to_cone_is_least {E : Type u_1} [ E] (s : set E) :
is_least {t : | s t} _)

theorem convex_hull_to_cone_eq_Inf {E : Type u_1} [ E] (s : set E) :
= Inf {t : | 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_1} [ E] (s : convex_cone E) (f : ) :
(∀ (x : (f.domain)), x s0 f x)(∀ (y : E), ∃ (x : (f.domain)), x + y s)f.domain (∃ (g : ), f < g ∀ (x : (g.domain)), x s0 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_1} [ E] (s : convex_cone E) (p : ) :
(∀ (x : (p.domain)), x s0 p x)(∀ (y : E), ∃ (x : (p.domain)), x + y s)(∃ (q : ) (H : q p), q.domain = ∀ (x : (q.domain)), x s0 q x)

theorem riesz_extension {E : Type u_1} [ E] (s : convex_cone E) (f : ) :
(∀ (x : (f.domain)), x s0 f x)(∀ (y : E), ∃ (x : (f.domain)), x + y s)(∃ (g : E →ₗ[] ), (∀ (x : (f.domain)), g x = f x) ∀ (x : E), x s0 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_1} [ E] (f : ) (N : E → ) :
(∀ (c : ), 0 < c∀ (x : E), N (c x) = c * N x)(∀ (x y : E), N (x + y) N x + N y)(∀ (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.