mathlib documentation

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:

Implementation notes

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

References

TODO

Definition of convex_cone and basic properties

structure convex_cone (E : Type u_1) [add_comm_group E] [vector_space 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]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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

@[simp]
theorem convex_cone.mem_mk {E : Type u_1} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space E] (S : convex_cone E) {c : } {x : E} :
0 < cx Sc x S

theorem convex_cone.add_mem {E : Type u_1} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space E] (S : convex_cone E) {c : } (hc : 0 < c) {x : E} :
c x S x S

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

@[instance]

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

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

@[instance]

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

@[instance]

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

@[instance]

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

@[instance]

Equations
def convex_cone.map {E : Type u_1} [add_comm_group E] [vector_space E] {F : Type u_2} [add_comm_group F] [vector_space 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} [add_comm_group E] [vector_space E] {F : Type u_2} [add_comm_group F] [vector_space F] {G : Type u_3} [add_comm_group G] [vector_space G] (g : F →ₗ[] G) (f : E →ₗ[] F) (S : convex_cone E) :

@[simp]

def convex_cone.comap {E : Type u_1} [add_comm_group E] [vector_space E] {F : Type u_2} [add_comm_group F] [vector_space F] :

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

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

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

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

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} [add_comm_group E] [vector_space E] :
convex_cone E → Prop

A convex cone is pointed if it includes 0.

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

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

Equations
def convex_cone.flat {E : Type u_1} [add_comm_group E] [vector_space E] :
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 {E : Type u_1} [add_comm_group E] [vector_space E] :
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_of_blunt {E : Type u_1} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space E] (S : convex_cone E) :

A pointed convex cone defines a preorder.

Equations

A pointed and salient cone defines a partial order.

Equations

A pointed and salient cone defines an ordered_add_comm_group.

Equations

Positive cone of an ordered semimodule

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

Equations

The positive cone of an ordered semimodule is always salient.

The positive cone of an ordered semimodule is always pointed.

Cone over a convex set

def convex.to_cone {E : Type u_1} [add_comm_group E] [vector_space 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} [add_comm_group E] [vector_space E] {s : set E} (hs : convex s) {x : E} :
x convex.to_cone s hs ∃ (c : ) (H : c > 0) (y : E) (H : y s), c y = x

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

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

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

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

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

theorem convex_hull_to_cone_eq_Inf {E : Type u_1} [add_comm_group E] [vector_space E] (s : set E) :

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} [add_comm_group E] [vector_space E] (s : convex_cone E) (f : linear_pmap E ) :
(∀ (x : (f.domain)), x s0 f x)(∀ (y : E), ∃ (x : (f.domain)), x + y s)f.domain (∃ (g : linear_pmap E ), 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} [add_comm_group E] [vector_space E] (s : convex_cone E) (p : linear_pmap E ) :
(∀ (x : (p.domain)), x s0 p x)(∀ (y : E), ∃ (x : (p.domain)), x + y s)(∃ (q : linear_pmap E ) (H : q p), q.domain = ∀ (x : (q.domain)), x s0 q x)

theorem riesz_extension {E : Type u_1} [add_comm_group E] [vector_space E] (s : convex_cone E) (f : linear_pmap E ) :
(∀ (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} [add_comm_group E] [vector_space E] (f : linear_pmap E ) (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.