mathlib documentation

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:

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 π•œ] [add_comm_monoid E] [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.

@[instance]
def convex_cone.set.has_coe {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_coe (convex_cone π•œ E) (set E)
Equations
@[instance]
def convex_cone.has_mem {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_mem E (convex_cone π•œ E)
Equations
@[instance]
def convex_cone.has_le {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_le (convex_cone π•œ E)
Equations
@[instance]
def convex_cone.has_lt {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_lt (convex_cone π•œ E)
Equations
@[simp]
theorem convex_cone.mem_coe {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S : convex_cone π•œ E) {x : E} :
@[simp]
theorem convex_cone.mem_mk {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [has_scalar π•œ E] {S T : convex_cone π•œ E} (h : ↑S = ↑T) :
S = T

Two convex_cones are equal if the underlying sets are equal.

theorem convex_cone.ext'_iff {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S : convex_cone π•œ E) ⦃x : E⦄ (hx : x ∈ S) ⦃y : E⦄ (hy : y ∈ S) :
x + y ∈ S
@[instance]
def convex_cone.has_inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_inf (convex_cone π•œ E)
Equations
theorem convex_cone.coe_inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S T : convex_cone π•œ E) :
theorem convex_cone.mem_inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S T : convex_cone π•œ E) {x : E} :
@[instance]
def convex_cone.has_Inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_Inf (convex_cone π•œ E)
Equations
theorem convex_cone.mem_Inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ 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 (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_bot (convex_cone π•œ E)
Equations
theorem convex_cone.mem_bot (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x : E) :
@[instance]
def convex_cone.has_top (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
has_top (convex_cone π•œ E)
Equations
theorem convex_cone.mem_top (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (x : E) :
@[instance]
def convex_cone.complete_lattice (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
Equations
@[instance]
def convex_cone.inhabited (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] :
inhabited (convex_cone π•œ E)
Equations
theorem convex_cone.convex {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (S : convex_cone π•œ E) :
convex π•œ ↑S
theorem convex_cone.smul_mem_iff {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [add_comm_monoid F] [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 π•œ] [add_comm_monoid E] [add_comm_monoid F] [add_comm_monoid G] [module π•œ E] [module π•œ F] [module π•œ G] (g : F β†’β‚—[π•œ] G) (f : E β†’β‚—[π•œ] F) (S : convex_cone π•œ E) :
@[simp]
theorem convex_cone.map_id {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_monoid E] [module π•œ E] (S : convex_cone π•œ E) :
def convex_cone.comap {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [linear_ordered_field π•œ] [add_comm_monoid E] [add_comm_monoid F] [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 π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [add_comm_monoid F] [add_comm_monoid G] [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 π•œ] [add_comm_monoid E] [add_comm_monoid F] [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 π•œ] [ordered_add_comm_group E] [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 π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [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 π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S : convex_cone π•œ E) :
theorem convex_cone.blunt_iff_not_pointed {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_scalar π•œ E] (S : convex_cone π•œ E) :
def convex_cone.flat {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [has_scalar π•œ E] (S : convex_cone π•œ E) :
theorem convex_cone.flat.pointed {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [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 π•œ] [add_comm_group E] [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 π•œ] [ordered_add_comm_group E] [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 π•œ] [ordered_add_comm_group E] [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 π•œ] [ordered_add_comm_group E] [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 π•œ] [ordered_add_comm_group E] [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 π•œ] [ordered_add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) {x : E} :
x ∈ convex.to_cone s 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 π•œ] [ordered_add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) {x : E} :
x ∈ convex.to_cone s hs ↔ βˆƒ (c : π•œ), 0 < c ∧ c β€’ x ∈ s
theorem convex.subset_to_cone {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [ordered_add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) :
theorem convex.to_cone_is_least {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [ordered_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 {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [ordered_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 {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [ordered_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 {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [ordered_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_2} [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_2} [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_2} [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_2} [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_5} [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_5} [inner_product_space ℝ H] (y : H) (s : set H) :
y ∈ s.inner_dual_cone ↔ βˆ€ (x : H), x ∈ s β†’ 0 ≀ inner x y