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 CompleteLattice, and define their images (ConvexCone.map) and preimages (ConvexCone.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.toCone to be the minimal cone that includes a given convex set.

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

In Mathlib/Analysis/Convex/Cone/Dual.lean, we prove the following theorems:

• ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem: This variant of the hyperplane separation theorem states that given a nonempty, closed, convex cone K in a complete, real inner product space H and a point b disjoint from it, there is a vector y which separates b from K in the sense that for all points x in K, 0 ≤ ⟪x, y⟫_ℝ and ⟪y, b⟫_ℝ < 0. This is also a geometric interpretation of the Farkas lemma.
• ConvexCone.inner_dual_cone_of_inner_dual_cone_eq_self:

Implementation notes

While Convex 𝕜 is a predicate on sets, ConvexCone 𝕜 E is a bundled convex cone.

References

• https://en.wikipedia.org/wiki/Convex_cone
• [Stephen P. Boyd and Lieven Vandenberghe, Convex Optimization][boydVandenberghe2004]
• [Emo Welzl and Bernd Gärtner, Cone Programming][welzl_garter]

Definition of ConvexCone and basic properties

structure ConvexCone (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Type u_2

• carrier : Set E
• smul_mem' : ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : E⦄, x ∈ s.carrier → c • x ∈ s.carrier
• add_mem' : ∀ ⦃x : E⦄, x ∈ s.carrier → ∀ ⦃y : E⦄, y ∈ s.carrier → x + y ∈ s.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.

instance ConvexCone.instSetLikeConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : SetLike (ConvexCone 𝕜 E) E

Equations

• ConvexCone.instSetLikeConvexCone = { coe := ConvexCone.carrier, coe_injective' := (_ : ∀ (S T : ConvexCone 𝕜 E), S.carrier = T.carrier → S = T) }

@[simp]

theorem ConvexCone.coe_mk {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [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 ConvexCone.mem_mk {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [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

theorem ConvexCone.ext {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} {T : ConvexCone 𝕜 E} (h : ∀ (x : E), x ∈ S ↔ x ∈ T) : S = T

Two ConvexCones are equal if they have the same elements.

theorem ConvexCone.smul_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) {c : 𝕜} {x : E} (hc : 0 < c) (hx : x ∈ S) : c • x ∈ S

theorem ConvexCone.add_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) ⦃x : E⦄ (hx : x ∈ S) ⦃y : E⦄ (hy : y ∈ S) : x + y ∈ S

instance ConvexCone.instAddMemClassConvexConeToAddToAddSemigroupToAddMonoidInstSetLikeConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : AddMemClass (ConvexCone 𝕜 E) E

Equations

• @ConvexCone.instAddMemClassConvexConeToAddToAddSemigroupToAddMonoidInstSetLikeConvexCone = @ConvexCone.instAddMemClassConvexConeToAddToAddSemigroupToAddMonoidInstSetLikeConvexCone.proof_1

instance ConvexCone.instInfConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Inf (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.coe_inf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) (T : ConvexCone 𝕜 E) : ↑(S ⊓ T) = ↑S ∩ ↑T

theorem ConvexCone.mem_inf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) (T : ConvexCone 𝕜 E) {x : E} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

instance ConvexCone.instInfSetConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : InfSet (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.coe_sInf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : Set (ConvexCone 𝕜 E)) : ↑(sInf S) = ⋂ (s : ConvexCone 𝕜 E) (_ : s ∈ S), ↑s

theorem ConvexCone.mem_sInf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {S : Set (ConvexCone 𝕜 E)} : x ∈ sInf S ↔ ∀ (s : ConvexCone 𝕜 E), s ∈ S → x ∈ s

@[simp]

theorem ConvexCone.coe_iInf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} (f : ι → ConvexCone 𝕜 E) : ↑(iInf f) = ⋂ (i : ι), ↑(f i)

theorem ConvexCone.mem_iInf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {ι : Sort u_5} {x : E} {f : ι → ConvexCone 𝕜 E} : x ∈ iInf f ↔ ∀ (i : ι), x ∈ f i

instance ConvexCone.instBotConvexCone (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Bot (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

theorem ConvexCone.mem_bot (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) : (x ∈ ⊥) = False

@[simp]

theorem ConvexCone.coe_bot (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : ↑⊥ = ∅

instance ConvexCone.instTopConvexCone (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Top (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

theorem ConvexCone.mem_top (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) : x ∈ ⊤

@[simp]

theorem ConvexCone.coe_top (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : ↑⊤ = Set.univ

instance ConvexCone.instCompleteLatticeConvexCone (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : CompleteLattice (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

instance ConvexCone.instInhabitedConvexCone (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Inhabited (ConvexCone 𝕜 E)

Equations

• ConvexCone.instInhabitedConvexCone 𝕜 = { default := ⊥ }

theorem ConvexCone.convex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : ConvexCone 𝕜 E) : Convex 𝕜 ↑S

def ConvexCone.map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : ConvexCone 𝕜 E) : ConvexCone 𝕜 F

The image of a convex cone under a 𝕜-linear map is a convex cone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.coe_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (S : ConvexCone 𝕜 E) (f : E →ₗ[𝕜] F) : ↑(ConvexCone.map f S) = ↑f '' ↑S

@[simp]

theorem ConvexCone.mem_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {f : E →ₗ[𝕜] F} {S : ConvexCone 𝕜 E} {y : F} : y ∈ ConvexCone.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

theorem ConvexCone.map_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [AddCommMonoid G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : ConvexCone 𝕜 E) : ConvexCone.map g (ConvexCone.map f S) = ConvexCone.map (LinearMap.comp g f) S

@[simp]

theorem ConvexCone.map_id {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : ConvexCone 𝕜 E) : ConvexCone.map LinearMap.id S = S

def ConvexCone.comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : ConvexCone 𝕜 F) : ConvexCone 𝕜 E

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.coe_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] (f : E →ₗ[𝕜] F) (S : ConvexCone 𝕜 F) : ↑(ConvexCone.comap f S) = ↑f ⁻¹' ↑S

@[simp]

theorem ConvexCone.comap_id {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : ConvexCone 𝕜 E) : ConvexCone.comap LinearMap.id S = S

theorem ConvexCone.comap_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [AddCommMonoid G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] (g : F →ₗ[𝕜] G) (f : E →ₗ[𝕜] F) (S : ConvexCone 𝕜 G) : ConvexCone.comap f (ConvexCone.comap g S) = ConvexCone.comap (LinearMap.comp g f) S

@[simp]

theorem ConvexCone.mem_comap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {f : E →ₗ[𝕜] F} {S : ConvexCone 𝕜 F} {x : E} : x ∈ ConvexCone.comap f S ↔ ↑f x ∈ S

theorem ConvexCone.smul_mem_iff {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommMonoid E] [MulAction 𝕜 E] (S : ConvexCone 𝕜 E) {c : 𝕜} (hc : 0 < c) {x : E} : c • x ∈ S ↔ x ∈ S

theorem ConvexCone.to_orderedSMul {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] (S : ConvexCone 𝕜 E) (h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S) : OrderedSMul 𝕜 E

Constructs an ordered module given an OrderedAddCommGroup, a cone, and a proof that the order relation is the one defined by the cone.

Convex cones with extra properties

def ConvexCone.Pointed {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : Prop

A convex cone is pointed if it includes 0.

Equations

• ConvexCone.Pointed S = (0 ∈ S)

def ConvexCone.Blunt {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : Prop

A convex cone is blunt if it doesn't include 0.

Equations

• ConvexCone.Blunt S = ¬0 ∈ S

theorem ConvexCone.pointed_iff_not_blunt {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : ConvexCone.Pointed S ↔ ¬ConvexCone.Blunt S

theorem ConvexCone.blunt_iff_not_pointed {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : ConvexCone.Blunt S ↔ ¬ConvexCone.Pointed S

theorem ConvexCone.Pointed.mono {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} {T : ConvexCone 𝕜 E} (h : S ≤ T) : ConvexCone.Pointed S → ConvexCone.Pointed T

theorem ConvexCone.Blunt.anti {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} {T : ConvexCone 𝕜 E} (h : T ≤ S) : ConvexCone.Blunt S → ConvexCone.Blunt T

def ConvexCone.Flat {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : Prop

A convex cone is flat if it contains some nonzero vector x and its opposite -x.

Equations

• ConvexCone.Flat S = ∃ x, x ∈ S ∧ x ≠ 0 ∧ -x ∈ S

def ConvexCone.Salient {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : Prop

A convex cone is salient if it doesn't include x and -x for any nonzero x.

Equations

• ConvexCone.Salient S = ∀ (x : E), x ∈ S → x ≠ 0 → ¬-x ∈ S

theorem ConvexCone.salient_iff_not_flat {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) : ConvexCone.Salient S ↔ ¬ConvexCone.Flat S

theorem ConvexCone.Flat.mono {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} {T : ConvexCone 𝕜 E} (h : S ≤ T) : ConvexCone.Flat S → ConvexCone.Flat T

theorem ConvexCone.Salient.anti {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} {T : ConvexCone 𝕜 E} (h : T ≤ S) : ConvexCone.Salient S → ConvexCone.Salient T

theorem ConvexCone.Flat.pointed {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} (hS : ConvexCone.Flat S) : ConvexCone.Pointed S

A flat cone is always pointed (contains 0).

theorem ConvexCone.Blunt.salient {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] {S : ConvexCone 𝕜 E} : ConvexCone.Blunt S → ConvexCone.Salient S

A blunt cone (one not containing 0) is always salient.

def ConvexCone.toPreorder {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) (h₁ : ConvexCone.Pointed S) : Preorder E

A pointed convex cone defines a preorder.

Equations

• ConvexCone.toPreorder S h₁ = Preorder.mk (_ : ∀ (x : E), x - x ∈ S) (_ : ∀ (x y z : E), x ≤ y → y ≤ z → x ≤ z)

def ConvexCone.toPartialOrder {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) (h₁ : ConvexCone.Pointed S) (h₂ : ConvexCone.Salient S) : PartialOrder E

A pointed and salient cone defines a partial order.

Equations

• ConvexCone.toPartialOrder S h₁ h₂ = let src := ConvexCone.toPreorder S h₁; PartialOrder.mk (_ : ∀ (a b : E), a ≤ b → b ≤ a → a = b)

def ConvexCone.toOrderedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [SMul 𝕜 E] (S : ConvexCone 𝕜 E) (h₁ : ConvexCone.Pointed S) (h₂ : ConvexCone.Salient S) : OrderedAddCommGroup E

A pointed and salient cone defines an OrderedAddCommGroup.

Equations

• One or more equations did not get rendered due to their size.

instance ConvexCone.instZeroConvexConeToSMulToZeroToAddMonoidToSMulZeroClassToZeroToMonoidWithZeroToSemiringToSMulWithZeroToMulActionWithZero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Zero (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.mem_zero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) : x ∈ 0 ↔ x = 0

@[simp]

theorem ConvexCone.coe_zero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ↑0 = 0

theorem ConvexCone.pointed_zero {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : ConvexCone.Pointed 0

instance ConvexCone.instAdd {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Add (ConvexCone 𝕜 E)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.mem_add {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {K₁ : ConvexCone 𝕜 E} {K₂ : ConvexCone 𝕜 E} {a : E} : a ∈ K₁ + K₂ ↔ ∃ x y, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = a

instance ConvexCone.instAddZeroClass {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : AddZeroClass (ConvexCone 𝕜 E)

Equations

• ConvexCone.instAddZeroClass = AddZeroClass.mk (_ : ∀ (x : ConvexCone 𝕜 E), 0 + x = x) (_ : ∀ (x : ConvexCone 𝕜 E), x + 0 = x)

instance ConvexCone.instAddCommSemigroup {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : AddCommSemigroup (ConvexCone 𝕜 E)

Equations

• ConvexCone.instAddCommSemigroup = AddCommSemigroup.mk (_ : ∀ (x x_1 : ConvexCone 𝕜 E), x + x_1 = x_1 + x)

Submodules are cones

def Submodule.toConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : Submodule 𝕜 E) : ConvexCone 𝕜 E

Every submodule is trivially a convex cone.

Equations

• Submodule.toConvexCone S = { carrier := ↑S, smul_mem' := (_ : ∀ (c : 𝕜), 0 < c → ∀ (x : E), x ∈ ↑S → c • x ∈ S), add_mem' := (_ : ∀ (x : E), x ∈ ↑S → ∀ (x_1 : E), x_1 ∈ ↑S → x + x_1 ∈ S) }

@[simp]

theorem Submodule.coe_toConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : Submodule 𝕜 E) : ↑(Submodule.toConvexCone S) = ↑S

@[simp]

theorem Submodule.mem_toConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {S : Submodule 𝕜 E} : x ∈ Submodule.toConvexCone S ↔ x ∈ S

@[simp]

theorem Submodule.toConvexCone_le_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {S : Submodule 𝕜 E} {T : Submodule 𝕜 E} : Submodule.toConvexCone S ≤ Submodule.toConvexCone T ↔ S ≤ T

@[simp]

theorem Submodule.toConvexCone_bot {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Submodule.toConvexCone ⊥ = 0

@[simp]

theorem Submodule.toConvexCone_top {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] : Submodule.toConvexCone ⊤ = ⊤

@[simp]

theorem Submodule.toConvexCone_inf {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : Submodule 𝕜 E) (T : Submodule 𝕜 E) : Submodule.toConvexCone (S ⊓ T) = Submodule.toConvexCone S ⊓ Submodule.toConvexCone T

@[simp]

theorem Submodule.pointed_toConvexCone {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (S : Submodule 𝕜 E) : ConvexCone.Pointed (Submodule.toConvexCone S)

Positive cone of an ordered module

def ConvexCone.positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone 𝕜 E

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.mem_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} : x ∈ ConvexCone.positive 𝕜 E ↔ 0 ≤ x

@[simp]

theorem ConvexCone.coe_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ↑(ConvexCone.positive 𝕜 E) = Set.Ici 0

theorem ConvexCone.salient_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone.Salient (ConvexCone.positive 𝕜 E)

The positive cone of an ordered module is always salient.

theorem ConvexCone.pointed_positive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone.Pointed (ConvexCone.positive 𝕜 E)

The positive cone of an ordered module is always pointed.

def ConvexCone.strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone 𝕜 E

The cone of strictly positive elements.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConvexCone.mem_strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} : x ∈ ConvexCone.strictlyPositive 𝕜 E ↔ 0 < x

@[simp]

theorem ConvexCone.coe_strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ↑(ConvexCone.strictlyPositive 𝕜 E) = Set.Ioi 0

theorem ConvexCone.positive_le_strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone.strictlyPositive 𝕜 E ≤ ConvexCone.positive 𝕜 E

theorem ConvexCone.salient_strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone.Salient (ConvexCone.strictlyPositive 𝕜 E)

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

theorem ConvexCone.blunt_strictlyPositive (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] : ConvexCone.Blunt (ConvexCone.strictlyPositive 𝕜 E)

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

Cone over a convex set

def Convex.toCone {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) (hs : Convex 𝕜 s) : ConvexCone 𝕜 E

The set of vectors proportional to those in a convex set forms a convex cone.

Equations

• One or more equations did not get rendered due to their size.

theorem Convex.mem_toCone {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} : x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ ∃ y, y ∈ s ∧ c • y = x

theorem Convex.mem_toCone' {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} : x ∈ Convex.toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s

theorem Convex.subset_toCone {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : s ⊆ ↑(Convex.toCone s hs)

theorem Convex.toCone_isLeast {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : IsLeast {t | s ⊆ ↑t} (Convex.toCone s hs)

hs.toCone s is the least cone that includes s.

theorem Convex.toCone_eq_sInf {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : Convex.toCone s hs = sInf {t | s ⊆ ↑t}

theorem convexHull_toCone_isLeast {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : IsLeast {t | s ⊆ ↑t} (Convex.toCone (↑(convexHull 𝕜) s) (_ : Convex 𝕜 (↑(convexHull 𝕜) s)))

theorem convexHull_toCone_eq_sInf {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : Convex.toCone (↑(convexHull 𝕜) s) (_ : Convex 𝕜 (↑(convexHull 𝕜) s)) = sInf {t | 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. RieszExtension.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 RieszExtension.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 RieszExtension.step {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ E) (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x) (dense : ∀ (y : E), ∃ x, ↑x + y ∈ s) (hdom : f.domain ≠ ⊤) : ∃ g, f < g ∧ ∀ (x : { x // 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 RieszExtension.exists_top {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ E) (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ (x : { x // x ∈ p.domain }), ↑x ∈ s → 0 ≤ ↑p x) (hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s) : ∃ q, q ≥ p ∧ q.domain = ⊤ ∧ ∀ (x : { x // x ∈ q.domain }), ↑x ∈ s → 0 ≤ ↑q x

theorem riesz_extension {E : Type u_2} [AddCommGroup E] [Module ℝ E] (s : ConvexCone ℝ E) (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ (x : { x // x ∈ f.domain }), ↑x ∈ s → 0 ≤ ↑f x) (dense : ∀ (y : E), ∃ x, ↑x + y ∈ s) : ∃ g, (∀ (x : { x // 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} [AddCommGroup 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 : { x // x ∈ f.domain }), ↑f x ≤ N ↑x) : ∃ g, (∀ (x : { x // 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.