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

Implementation notes #

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

References #

Definition of convex_cone and basic properties #

structure convex_cone (E : Type u_1) [add_comm_group E] [module 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} [add_comm_group E] [module E] :
Equations
@[instance]
def convex_cone.has_mem {E : Type u_1} [add_comm_group E] [module E] :
Equations
@[instance]
def convex_cone.has_le {E : Type u_1} [add_comm_group E] [module E] :
Equations
@[instance]
def convex_cone.has_lt {E : Type u_1} [add_comm_group E] [module E] :
Equations
@[simp]
theorem convex_cone.mem_coe {E : Type u_1} [add_comm_group E] [module 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] [module 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] [module E] {S T : convex_cone E} (h : S = T) :
S = 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] [module 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] [module 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 {E : Type u_1} [add_comm_group E] [module E] (S : convex_cone E) {c : } {x : E} (hc : 0 < c) (hx : x S) :
c x S
theorem convex_cone.add_mem {E : Type u_1} [add_comm_group E] [module E] (S : convex_cone E) ⦃x : E⦄ (hx : x S) ⦃y : E⦄ (hy : y S) :
x + y S
theorem convex_cone.smul_mem_iff {E : Type u_1} [add_comm_group E] [module 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] [module E] (S : convex_cone E) :
@[instance]
def convex_cone.has_inf {E : Type u_1} [add_comm_group E] [module E] :
Equations
theorem convex_cone.coe_inf {E : Type u_1} [add_comm_group E] [module E] (S T : convex_cone E) :
(S T) = S T
theorem convex_cone.mem_inf {E : Type u_1} [add_comm_group E] [module 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} [add_comm_group E] [module E] :
Equations
theorem convex_cone.mem_Inf {E : Type u_1} [add_comm_group E] [module E] {x : E} {S : set (convex_cone E)} :
x Inf S ∀ (s : convex_cone E), s Sx s
@[instance]
def convex_cone.has_bot {E : Type u_1} [add_comm_group E] [module E] :
Equations
theorem convex_cone.mem_bot {E : Type u_1} [add_comm_group E] [module E] (x : E) :
@[instance]
def convex_cone.has_top {E : Type u_1} [add_comm_group E] [module E] :
Equations
theorem convex_cone.mem_top {E : Type u_1} [add_comm_group E] [module E] (x : E) :
@[instance]
Equations
@[instance]
Equations
def convex_cone.map {E : Type u_1} [add_comm_group E] [module E] {F : Type u_2} [add_comm_group F] [module F] (f : E →ₗ[] F) (S : convex_cone E) :

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] [module E] {F : Type u_2} [add_comm_group F] [module F] {G : Type u_3} [add_comm_group G] [module G] (g : F →ₗ[] G) (f : E →ₗ[] F) (S : convex_cone E) :
@[simp]
theorem convex_cone.map_id {E : Type u_1} [add_comm_group E] [module E] (S : convex_cone E) :
def convex_cone.comap {E : Type u_1} [add_comm_group E] [module E] {F : Type u_2} [add_comm_group F] [module F] (f : E →ₗ[] F) (S : convex_cone F) :

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

Equations
@[simp]
theorem convex_cone.comap_comap {E : Type u_1} [add_comm_group E] [module E] {F : Type u_2} [add_comm_group F] [module F] {G : Type u_3} [add_comm_group G] [module 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] [module E] {F : Type u_2} [add_comm_group F] [module F] {f : E →ₗ[] F} {S : convex_cone F} {x : E} :
theorem convex_cone.to_ordered_module {M : Type u_1} [ordered_add_comm_group M] [module M] (S : convex_cone M) (h : ∀ (x y : M), x y y - x S) :

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 {E : Type u_1} [add_comm_group E] [module E] (S : 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] [module E] (S : 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] [module 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 {E : Type u_1} [add_comm_group E] [module 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_of_blunt {E : Type u_1} [add_comm_group E] [module 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] [module E] (S : convex_cone E) (h₁ : S.pointed) :

A pointed convex cone defines a preorder.

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

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

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

Equations

The positive cone of an ordered module is always salient.

The positive cone of an ordered module is always pointed.

Cone over a convex set #

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

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] [module 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] [module 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] [module E] {s : set E} (hs : convex s) :
theorem convex.to_cone_is_least {E : Type u_1} [add_comm_group E] [module 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] [module E] {s : set E} (hs : convex s) :
theorem convex_hull_to_cone_is_least {E : Type u_1} [add_comm_group E] [module E] (s : set E) :
theorem convex_hull_to_cone_eq_Inf {E : Type u_1} [add_comm_group E] [module 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] [module E] (s : convex_cone E) (f : linear_pmap E ) (nonneg : ∀ (x : (f.domain)), x s0 f x) (dense : ∀ (y : E), ∃ (x : (f.domain)), x + y s) (hdom : 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] [module E] (s : convex_cone E) (p : linear_pmap E ) (hp_nonneg : ∀ (x : (p.domain)), x s0 p x) (hp_dense : ∀ (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] [module E] (s : convex_cone E) (f : linear_pmap E ) (nonneg : ∀ (x : (f.domain)), x s0 f x) (dense : ∀ (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] [module E] (f : linear_pmap 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.

The dual cone #

def set.inner_dual_cone {H : Type u_4} [inner_product_space H] (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_4} [inner_product_space H] (y : H) (s : set H) :
y s.inner_dual_cone ∀ (x : H), x s0 inner x y