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:

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 𝕜 E is a bundled convex cone.

References #

https://en.wikipedia.org/wiki/Convex_cone

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

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

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.

@[protected, 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

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

@[protected, 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

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

@[protected, 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

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

@[protected, 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

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

@[simp, norm_cast]

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

x ∈ ↑S ↔ x ∈ S

@[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.

@[protected]

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

↑S = ↑T ↔ S = T

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

c • 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

@[protected, 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

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

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

↑(S ⊓ T) = ↑S ∩ ↑T

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

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

@[protected, 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

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

@[protected, 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

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

theorem convex_cone.mem_bot (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x : E) :

x ∈ ⊥ = false

@[protected, 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

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

theorem convex_cone.mem_top (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 E] (x : E) :

@[protected, instance]

def convex_cone.complete_lattice (𝕜 : Type u_1) {E : Type u_2} [ordered_semiring 𝕜] [add_comm_monoid E] [has_scalar 𝕜 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 := _, 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 := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

@[protected, 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

convex_cone.inhabited 𝕜 = {default := ⊥}

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

c • x ∈ S ↔ x ∈ S

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

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

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

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

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

convex_cone.map linear_map.id S = S

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

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

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

convex_cone.comap linear_map.id S = S

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

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

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

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

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

S.pointed = (0 ∈ S)

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

S.blunt = (0 ∉ S)

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

S.pointed ↔ ¬S.blunt

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

S.blunt ↔ ¬S.pointed

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

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

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

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

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

S.salient ↔ ¬S.flat

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

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

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

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_2), add_assoc := _, zero := add_comm_group.zero (show add_comm_group E, from _inst_2), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (show add_comm_group E, from _inst_2), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (show add_comm_group E, from _inst_2), sub := add_comm_group.sub (show add_comm_group E, from _inst_2), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (show add_comm_group E, from _inst_2), zsmul_zero' := _, zsmul_succ' := _, zsmul_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 (𝕜 : 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

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

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

(convex_cone.positive_cone 𝕜 E).salient

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

(convex_cone.positive_cone 𝕜 E).pointed

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

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

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

s ⊆ ↑(convex.to_cone s hs)

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 #

noncomputable def set.inner_dual_cone {H : Type u_5} [inner_product_space ℝ H] (s : set H) :

convex_cone ℝ 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_5} [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_5} [inner_product_space ℝ H] :

∅.inner_dual_cone = ⊤

theorem inner_dual_cone_le_inner_dual_cone {H : Type u_5} [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_5} [inner_product_space ℝ H] (s : set H) :

s.inner_dual_cone.pointed