mathlib documentation

analysis.convex.cone.basic

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

We prove the following 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_smul π•œ 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.

Instances for convex_cone
@[protected, instance]
def convex_cone.set_like {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
set_like (convex_cone π•œ E) E
Equations
@[simp]
theorem convex_cone.coe_mk {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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} :
↑{carrier := s, smul_mem' := h₁, add_mem' := hβ‚‚} = s
@[simp]
theorem convex_cone.mem_mk {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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
@[ext]
theorem convex_cone.ext {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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_smul π•œ 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_smul π•œ E] (S : convex_cone π•œ E) ⦃x : E⦄ (hx : x ∈ S) ⦃y : E⦄ (hy : y ∈ S) :
x + y ∈ S
@[protected, instance]
def convex_cone.add_mem_class {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
add_mem_class (convex_cone π•œ E) E
Equations
@[protected, instance]
def convex_cone.has_inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
has_inf (convex_cone π•œ E)
Equations
@[simp]
theorem convex_cone.coe_inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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_smul π•œ E] (S T : convex_cone π•œ E) {x : E} :
@[protected, instance]
def convex_cone.has_Inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
has_Inf (convex_cone π•œ E)
Equations
@[simp]
theorem convex_cone.coe_Inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] (S : set (convex_cone π•œ E)) :
↑(has_Inf.Inf S) = β‹‚ (s : convex_cone π•œ E) (H : s ∈ S), ↑s
theorem convex_cone.mem_Inf {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {x : E} {S : set (convex_cone π•œ E)} :
@[simp]
theorem convex_cone.coe_infi {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {ΞΉ : Sort u_3} (f : ΞΉ β†’ convex_cone π•œ E) :
↑(infi f) = β‹‚ (i : ΞΉ), ↑(f i)
theorem convex_cone.mem_infi {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {ΞΉ : Sort u_3} {x : E} {f : ΞΉ β†’ convex_cone π•œ E} :
x ∈ infi f ↔ βˆ€ (i : ΞΉ), x ∈ f i
@[protected, instance]
def convex_cone.has_bot (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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_smul π•œ E] (x : E) :
@[simp]
theorem convex_cone.coe_bot (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
@[protected, instance]
def convex_cone.has_top (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ 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_smul π•œ E] (x : E) :
@[simp]
theorem convex_cone.coe_top (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
@[protected, instance]
def convex_cone.complete_lattice (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
Equations
@[protected, instance]
def convex_cone.inhabited (π•œ : Type u_1) {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] :
inhabited (convex_cone π•œ E)
Equations
@[protected]
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
@[simp]
theorem convex_cone.mem_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} {y : F} :
y ∈ convex_cone.map f S ↔ βˆƒ (x : E) (H : x ∈ S), ⇑f x = y
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.coe_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) :
@[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_smul π•œ 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_smul π•œ 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_smul π•œ 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_smul π•œ E] (S : convex_cone π•œ E) :
theorem convex_cone.pointed.mono {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {S T : convex_cone π•œ E} (h : S ≀ T) :
theorem convex_cone.blunt.anti {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [has_smul π•œ E] {S T : convex_cone π•œ E} (h : T ≀ S) :
def convex_cone.flat {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [has_smul π•œ 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_smul π•œ 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_smul π•œ E] (S : convex_cone π•œ E) :
theorem convex_cone.flat.mono {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [has_smul π•œ E] {S T : convex_cone π•œ E} (h : S ≀ T) :
theorem convex_cone.salient.anti {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [has_smul π•œ E] {S T : convex_cone π•œ E} (h : T ≀ S) :
theorem convex_cone.flat.pointed {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_group E] [has_smul π•œ 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_smul π•œ E] {S : convex_cone π•œ E} :

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_smul π•œ 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_smul π•œ 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_smul π•œ E] (S : convex_cone π•œ E) (h₁ : S.pointed) (hβ‚‚ : S.salient) :

A pointed and salient cone defines an ordered_add_comm_group.

Equations
@[protected, instance]
def convex_cone.has_zero {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
has_zero (convex_cone π•œ E)
Equations
@[simp]
theorem convex_cone.mem_zero {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] (x : E) :
x ∈ 0 ↔ x = 0
@[simp]
theorem convex_cone.coe_zero {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
theorem convex_cone.pointed_zero {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
@[protected, instance]
def convex_cone.has_add {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
has_add (convex_cone π•œ E)
Equations
@[simp]
theorem convex_cone.mem_add {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] {K₁ Kβ‚‚ : convex_cone π•œ E} {a : E} :
a ∈ K₁ + Kβ‚‚ ↔ βˆƒ (x y : E), x ∈ K₁ ∧ y ∈ Kβ‚‚ ∧ x + y = a
@[protected, instance]
def convex_cone.add_zero_class {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
Equations
@[protected, instance]
def convex_cone.add_comm_semigroup {π•œ : Type u_1} {E : Type u_2} [ordered_semiring π•œ] [add_comm_monoid E] [module π•œ E] :
Equations

Positive cone of an ordered module #

def convex_cone.positive (π•œ : 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
@[simp]
theorem convex_cone.mem_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] {x : E} :
@[simp]
theorem convex_cone.coe_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :
theorem convex_cone.salient_positive (π•œ : 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 (π•œ : 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.

def convex_cone.strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :
convex_cone π•œ E

The cone of strictly positive elements.

Note that this naming diverges from the mathlib convention of pos and nonneg due to "positive cone" (convex_cone.positive) being established terminology for the non-negative elements.

Equations
@[simp]
theorem convex_cone.mem_strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] {x : E} :
@[simp]
theorem convex_cone.coe_strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :
theorem convex_cone.positive_le_strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :
theorem convex_cone.salient_strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :

The strictly positive cone of an ordered module is always salient.

theorem convex_cone.blunt_strictly_positive (π•œ : Type u_1) (E : Type u_2) [ordered_semiring π•œ] [ordered_add_comm_group E] [module π•œ E] [ordered_smul π•œ E] :

The strictly positive cone of an ordered module is always blunt.

Cone over a convex set #

def convex.to_cone {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [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 π•œ] [add_comm_group E] [module π•œ E] {s : set E} (hs : convex π•œ s) :
theorem convex_hull_to_cone_is_least {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [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 π•œ] [add_comm_group E] [module π•œ E] (s : set E) :
convex.to_cone (⇑(convex_hull π•œ) s) _ = has_Inf.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.

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 {E : Type u_2} [add_comm_group E] [module ℝ E] (s : convex_cone ℝ E) (f : E β†’β‚—.[ℝ] ℝ) (nonneg : βˆ€ (x : β†₯(f.domain)), ↑x ∈ s β†’ 0 ≀ ⇑f x) (dense : βˆ€ (y : E), βˆƒ (x : β†₯(f.domain)), ↑x + y ∈ s) :

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

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 #

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
@[simp]
@[simp]

Dual cone of the convex cone {0} is the total space.

@[simp]

Dual cone of the total space is the convex cone {0}.

The inner dual cone of a singleton is given by the preimage of the positive cone under the linear map Ξ» y, βŸͺx, y⟫.

theorem inner_dual_cone_Union {H : Type u_5} [inner_product_space ℝ H] {ΞΉ : Sort u_1} (f : ΞΉ β†’ set H) :
(⋃ (i : ΞΉ), f i).inner_dual_cone = β¨… (i : ΞΉ), (f i).inner_dual_cone

The dual cone of s equals the intersection of dual cones of the points in s.

This is a stronger version of the Hahn-Banach separation theorem for closed convex cones. This is also the geometric interpretation of Farkas' lemma.

The inner dual of inner dual of a non-empty, closed convex cone is itself.