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:

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

Definition of `convex_cone` and basic properties #

structure convex_cone (E : Type u_1) [add_comm_group E] [module ℝ E] :

Type u_1

carrier : set E
smul_mem' : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ ⦃x : E⦄, x ∈ c.carrier → c_1 • x ∈ c.carrier
add_mem' : ∀ ⦃x : E⦄, x ∈ c.carrier → ∀ ⦃y : E⦄, y ∈ c.carrier → x + y ∈ c.carrier

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

has_coe (convex_cone E) (set E)

Equations

convex_cone.set.has_coe = {coe := convex_cone.carrier _inst_2}

@[instance]

def convex_cone.has_mem {E : Type u_1} [add_comm_group E] [module ℝ E] :

has_mem E (convex_cone E)

Equations

convex_cone.has_mem = {mem := λ (m : E) (S : convex_cone E), m ∈ S.carrier}

@[instance]

def convex_cone.has_le {E : Type u_1} [add_comm_group E] [module ℝ E] :

has_le (convex_cone E)

Equations

convex_cone.has_le = {le := λ (S T : convex_cone E), S.carrier ⊆ T.carrier}

@[instance]

def convex_cone.has_lt {E : Type u_1} [add_comm_group E] [module ℝ E] :

has_lt (convex_cone E)

Equations

convex_cone.has_lt = {lt := λ (S T : convex_cone E), S.carrier ⊂ T.carrier}

@[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 ∈ 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' {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] :

has_inf (convex_cone E)

Equations

convex_cone.has_inf = {inf := λ (S T : convex_cone E), {carrier := ↑S ∩ ↑T, smul_mem' := _, add_mem' := _}}

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

has_Inf (convex_cone E)

Equations

convex_cone.has_Inf = {Inf := λ (S : set (convex_cone E)), {carrier := ⋂ (s : convex_cone E) (H : s ∈ S), ↑s, smul_mem' := _, add_mem' := _}}

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 ∈ S → x ∈ s

@[instance]

def convex_cone.has_bot {E : Type u_1} [add_comm_group E] [module ℝ E] :

has_bot (convex_cone E)

Equations

convex_cone.has_bot = {bot := {carrier := ∅, smul_mem' := _, add_mem' := _}}

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

x ∈ ⊥ = false

@[instance]

def convex_cone.has_top {E : Type u_1} [add_comm_group E] [module ℝ E] :

has_top (convex_cone E)

Equations

convex_cone.has_top = {top := {carrier := set.univ E, smul_mem' := _, add_mem' := _}}

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

@[instance]

def convex_cone.complete_lattice {E : Type u_1} [add_comm_group E] [module ℝ E] :

complete_lattice (convex_cone E)

Equations

convex_cone.complete_lattice = {sup := λ (a b : convex_cone E), Inf {x : convex_cone E | a ≤ x ∧ b ≤ x}, le := has_le.le convex_cone.has_le, lt := has_lt.lt convex_cone.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf convex_cone.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := ⊤, le_top := _, bot := ⊥, bot_le := _, Sup := λ (s : set (convex_cone E)), Inf {T : convex_cone E | ∀ (S : convex_cone E), S ∈ s → S ≤ T}, le_Sup := _, Sup_le := _, Inf := Inf convex_cone.has_Inf, Inf_le := _, le_Inf := _}

@[instance]

def convex_cone.inhabited {E : Type u_1} [add_comm_group E] [module ℝ E] :

inhabited (convex_cone E)

Equations

convex_cone.inhabited = {default := ⊥}

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

convex_cone.map f S = {carrier := ⇑f '' ↑S, smul_mem' := _, add_mem' := _}

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

convex_cone.map g (convex_cone.map f S) = convex_cone.map (g.comp f) S

@[simp]

theorem convex_cone.map_id {E : Type u_1} [add_comm_group E] [module ℝ E] (S : convex_cone E) :

convex_cone.map linear_map.id S = S

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

convex_cone.comap f S = {carrier := ⇑f ⁻¹' ↑S, smul_mem' := _, add_mem' := _}

@[simp]

theorem convex_cone.comap_id {E : Type u_1} [add_comm_group E] [module ℝ E] (S : convex_cone E) :

convex_cone.comap linear_map.id S = S

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

convex_cone.comap f (convex_cone.comap g S) = convex_cone.comap (g.comp f) S

@[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} :

x ∈ convex_cone.comap f S ↔ ⇑f x ∈ S

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

ordered_module ℝ M

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

S.pointed = (0 ∈ S)

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

S.blunt = (0 ∉ S)

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

S.flat = ∃ (x : E) (H : x ∈ S), x ≠ 0 ∧ -x ∈ S

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

S.salient = ∀ (x : E), x ∈ S → x ≠ 0 → -x ∉ S

theorem convex_cone.pointed_iff_not_blunt {E : Type u_1} [add_comm_group E] [module ℝ E] (S : convex_cone E) :

S.pointed ↔ ¬S.blunt

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

S.salient ↔ ¬S.flat

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

S.to_preorder h₁ = {le := λ (x y : E), y - x ∈ S, lt := λ (a b : E), b - a ∈ S ∧ a - b ∉ S, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

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

partial_order E

A pointed and salient cone defines a partial order.

Equations

S.to_partial_order h₁ h₂ = {le := preorder.le (S.to_preorder h₁), lt := preorder.lt (S.to_preorder h₁), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

ordered_add_comm_group E

A pointed and salient cone defines an ordered_add_comm_group.

Equations

S.to_ordered_add_comm_group h₁ h₂ = {add := add_comm_group.add (show add_comm_group E, from _inst_1), add_assoc := _, zero := add_comm_group.zero (show add_comm_group E, from _inst_1), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (show add_comm_group E, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (show add_comm_group E, from _inst_1), sub := add_comm_group.sub (show add_comm_group E, from _inst_1), sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (show add_comm_group E, from _inst_1), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (S.to_partial_order h₁ h₂), lt := partial_order.lt (S.to_partial_order h₁ h₂), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

Positive cone of an ordered module #

def convex_cone.positive_cone (M : Type u_4) [ordered_add_comm_group M] [module ℝ M] [ordered_module ℝ M] :

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

Equations

convex_cone.positive_cone M = {carrier := {x : M | 0 ≤ x}, smul_mem' := _, add_mem' := _}

theorem convex_cone.salient_of_positive_cone (M : Type u_4) [ordered_add_comm_group M] [module ℝ M] [ordered_module ℝ M] :

(convex_cone.positive_cone M).salient

The positive cone of an ordered module is always salient.

theorem convex_cone.pointed_of_positive_cone (M : Type u_4) [ordered_add_comm_group M] [module ℝ M] [ordered_module ℝ M] :

(convex_cone.positive_cone M).pointed

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

convex.to_cone s hs = {carrier := ⋃ (c : ℝ) (H : c > 0), c • s, smul_mem' := _, add_mem' := _}

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

s ⊆ ↑(convex.to_cone s hs)

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

is_least {t : convex_cone E | s ⊆ ↑t} (convex.to_cone s hs)

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

convex.to_cone s hs = Inf {t : convex_cone E | s ⊆ ↑t}

theorem convex_hull_to_cone_is_least {E : Type u_1} [add_comm_group E] [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 {E : Type u_1} [add_comm_group E] [module ℝ E] (s : set E) :

convex.to_cone (⇑convex_hull s) _ = 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_1} [add_comm_group E] [module ℝ E] (s : convex_cone E) (f : linear_pmap ℝ E ℝ) (nonneg : ∀ (x : ↥(f.domain)), ↑x ∈ s → 0 ≤ ⇑f x) (dense : ∀ (y : E), ∃ (x : ↥(f.domain)), ↑x + y ∈ s) (hdom : f.domain ≠ ⊤) :

∃ (g : linear_pmap ℝ 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_1} [add_comm_group E] [module ℝ E] (s : convex_cone E) (p : linear_pmap ℝ E ℝ) (hp_nonneg : ∀ (x : ↥(p.domain)), ↑x ∈ s → 0 ≤ ⇑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 ∈ s → 0 ≤ ⇑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 ∈ 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_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

s.inner_dual_cone = {carrier := {y : H | ∀ (x : H), x ∈ s → 0 ≤ inner x y}, smul_mem' := _, add_mem' := _}

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 ∈ s → 0 ≤ inner x y

@[simp]

theorem inner_dual_cone_empty {H : Type u_4} [inner_product_space ℝ H] :

∅.inner_dual_cone = ⊤

theorem inner_dual_cone_le_inner_dual_cone {H : Type u_4} [inner_product_space ℝ H] (s t : set H) (h : t ⊆ s) :

s.inner_dual_cone ≤ t.inner_dual_cone

theorem pointed_inner_dual_cone {H : Type u_4} [inner_product_space ℝ H] (s : set H) :

s.inner_dual_cone.pointed