Convex cones

In an R-module M, 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

In Mathlib/Analysis/Convex/Cone/Extension.lean we prove the M. Riesz extension theorem and a form of the Hahn-Banach theorem.

In Mathlib/Analysis/Convex/Cone/Dual.lean we prove a variant of the hyperplane separation theorem.

Implementation notes

While Convex R is a predicate on sets, ConvexCone R M 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 (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : Type u_4

A convex cone is a subset s of an R-module such that a • x + b • y ∈ s whenever a, b > 0 and x, y ∈ s.

• carrier : Set M

  The carrier set underlying this cone: the set of points contained in it

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

instance ConvexCone.instSetLike {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : SetLike (ConvexCone R M) M

Equations

• ConvexCone.instSetLike = { coe := ConvexCone.carrier, coe_injective' := ⋯ }

@[simp]

theorem ConvexCone.coe_mk {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (s : Set M) (h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s) (h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s) : ↑{ carrier := s, smul_mem' := h₁, add_mem' := h₂ } = s

@[simp]

theorem ConvexCone.mem_mk {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {s : Set M} {x : M} {h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s} {h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s} : x ∈ { carrier := s, smul_mem' := h₁, add_mem' := h₂ } ↔ x ∈ s

theorem ConvexCone.ext {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} (h : ∀ (x : M), x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂

Two ConvexCones are equal if they have the same elements.

theorem ConvexCone.ext_iff {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} : C₁ = C₂ ↔ ∀ (x : M), x ∈ C₁ ↔ x ∈ C₂

theorem ConvexCone.smul_mem {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) {c : R} {x : M} (hc : 0 < c) (hx : x ∈ C) : c • x ∈ C

theorem ConvexCone.add_mem {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) ⦃x : M⦄ (hx : x ∈ C) ⦃y : M⦄ (hy : y ∈ C) : x + y ∈ C

instance ConvexCone.instAddMemClass {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : AddMemClass (ConvexCone R M) M

def ConvexCone.copy {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) (s : Set M) (hs : s = ↑C) : ConvexCone R M

Copy of a convex cone with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• C.copy s hs = { carrier := s, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem ConvexCone.copy_carrier {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) (s : Set M) (hs : s = ↑C) : ↑(C.copy s hs) = s

theorem ConvexCone.copy_eq {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) (s : Set M) (hs : s = ↑C) : C.copy s hs = C

instance ConvexCone.instInfSet {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : InfSet (ConvexCone R M)

Equations

• ConvexCone.instInfSet = { sInf := fun (S : Set (ConvexCone R M)) => { carrier := ⋂ C ∈ S, ↑C, smul_mem' := ⋯, add_mem' := ⋯ } }

@[simp]

theorem ConvexCone.coe_sInf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (S : Set (ConvexCone R M)) : ↑(sInf S) = ⋂ C ∈ S, ↑C

@[simp]

theorem ConvexCone.mem_sInf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {x : M} {S : Set (ConvexCone R M)} : x ∈ sInf S ↔ ∀ C ∈ S, x ∈ C

@[simp]

theorem ConvexCone.coe_iInf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {ι : Sort u_7} (f : ι → ConvexCone R M) : ↑(iInf f) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem ConvexCone.mem_iInf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {x : M} {ι : Sort u_7} {f : ι → ConvexCone R M} : x ∈ iInf f ↔ ∀ (i : ι), x ∈ f i

instance ConvexCone.instCompleteSemilatticeInf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : CompleteSemilatticeInf (ConvexCone R M)

Equations

• ConvexCone.instCompleteSemilatticeInf = { toPartialOrder := SetLike.instPartialOrder, toInfSet := ConvexCone.instInfSet, sInf_le := ⋯, le_sInf := ⋯ }

def ConvexCone.hull (R : Type u_2) {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (s : Set M) : ConvexCone R M

The cone hull of a set. The smallest convex cone containing that set.

Equations

• ConvexCone.hull R s = sInf {C : ConvexCone R M | s ⊆ ↑C}

theorem ConvexCone.subset_hull {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {s : Set M} : s ⊆ ↑(hull R s)

theorem ConvexCone.hull_min {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C : ConvexCone R M} {s : Set M} (hsC : s ⊆ ↑C) : hull R s ≤ C

theorem ConvexCone.hull_le_iff {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C : ConvexCone R M} {s : Set M} : hull R s ≤ C ↔ s ⊆ ↑C

theorem ConvexCone.gc_hull_coe {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : GaloisConnection (hull R) SetLike.coe

def ConvexCone.gi {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : GaloisInsertion (hull R) SetLike.coe

Galois insertion between ConvexCone and SetLike.coe.

Equations

• ConvexCone.gi = { choice := fun (s : Set M) (hs : ↑(ConvexCone.hull R s) ≤ s) => (ConvexCone.hull R s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

instance ConvexCone.instBot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : Bot (ConvexCone R M)

Equations

• ConvexCone.instBot = { bot := { carrier := ∅, smul_mem' := ⋯, add_mem' := ⋯ } }

@[simp]

theorem ConvexCone.notMem_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {x : M} : x ∉ ⊥

@[deprecated ConvexCone.notMem_bot (since := "2025-06-11")]

theorem ConvexCone.mem_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (x : M) : (x ∈ ⊥) = False

@[simp]

theorem ConvexCone.coe_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : ↑⊥ = ∅

@[simp]

theorem ConvexCone.coe_eq_empty {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C : ConvexCone R M} : ↑C = ∅ ↔ C = ⊥

instance ConvexCone.instCompleteLattice {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : CompleteLattice (ConvexCone R M)

Equations

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

@[simp]

theorem ConvexCone.coe_inf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C₁ C₂ : ConvexCone R M) : ↑(C₁ ⊓ C₂) = ↑C₁ ∩ ↑C₂

@[simp]

theorem ConvexCone.mem_inf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} {x : M} : x ∈ C₁ ⊓ C₂ ↔ x ∈ C₁ ∧ x ∈ C₂

@[simp]

theorem ConvexCone.mem_top {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {x : M} : x ∈ ⊤

@[simp]

theorem ConvexCone.coe_top {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : ↑⊤ = Set.univ

@[simp]

theorem ConvexCone.disjoint_coe {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} : Disjoint ↑C₁ ↑C₂ ↔ Disjoint C₁ C₂

instance ConvexCone.instInhabited {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] : Inhabited (ConvexCone R M)

Equations

• ConvexCone.instInhabited = { default := ⊥ }

theorem ConvexCone.convex {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : ConvexCone R M) : Convex R ↑C

def ConvexCone.map {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (C : ConvexCone R M) : ConvexCone R N

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

Equations

• ConvexCone.map f C = { carrier := ⇑f '' ↑C, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem ConvexCone.coe_map {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (C : ConvexCone R M) (f : M →ₗ[R] N) : ↑(map f C) = ⇑f '' ↑C

@[simp]

theorem ConvexCone.mem_map {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} {C : ConvexCone R M} {y : N} : y ∈ map f C ↔ ∃ x ∈ C, f x = y

theorem ConvexCone.map_map {R : Type u_2} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] [Module R M] [Module R N] [Module R O] (g : N →ₗ[R] O) (f : M →ₗ[R] N) (C : ConvexCone R M) : map g (map f C) = map (g ∘ₗ f) C

@[simp]

theorem ConvexCone.map_id {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : ConvexCone R M) : map LinearMap.id C = C

def ConvexCone.comap {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (C : ConvexCone R N) : ConvexCone R M

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

Equations

• ConvexCone.comap f C = { carrier := ⇑f ⁻¹' ↑C, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem ConvexCone.coe_comap {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (C : ConvexCone R N) : ↑(comap f C) = ⇑f ⁻¹' ↑C

@[simp]

theorem ConvexCone.comap_id {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : ConvexCone R M) : comap LinearMap.id C = C

theorem ConvexCone.comap_comap {R : Type u_2} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] [Module R M] [Module R N] [Module R O] (g : N →ₗ[R] O) (f : M →ₗ[R] N) (C : ConvexCone R O) : comap f (comap g C) = comap (g ∘ₗ f) C

@[simp]

theorem ConvexCone.mem_comap {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {f : M →ₗ[R] N} {C : ConvexCone R N} {x : M} : x ∈ comap f C ↔ f x ∈ C

theorem ConvexCone.smul_mem_iff {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid M] [MulAction 𝕜 M] (C : ConvexCone 𝕜 M) {c : 𝕜} (hc : 0 < c) {x : M} : c • x ∈ C ↔ x ∈ C

Convex cones with extra properties

def ConvexCone.Pointed {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) : Prop

A convex cone is pointed if it includes 0.

Equations

• C.Pointed = (0 ∈ C)

def ConvexCone.Blunt {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] (C : ConvexCone R M) : Prop

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

Equations

• C.Blunt = (0 ∉ C)

theorem ConvexCone.blunt_iff_not_pointed {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C : ConvexCone R M} : C.Blunt ↔ ¬C.Pointed

theorem ConvexCone.pointed_iff_not_blunt {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C : ConvexCone R M} : C.Pointed ↔ ¬C.Blunt

theorem ConvexCone.Pointed.mono {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} (h : C₁ ≤ C₂) : C₁.Pointed → C₂.Pointed

theorem ConvexCone.Blunt.anti {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] {C₁ C₂ : ConvexCone R M} (h : C₂ ≤ C₁) : C₁.Blunt → C₂.Blunt

def ConvexCone.Flat {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) : Prop

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

Equations

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

def ConvexCone.Salient {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) : Prop

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

Equations

• C.Salient = ∀ x ∈ C, x ≠ 0 → -x ∉ C

theorem ConvexCone.salient_iff_not_flat {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] {C : ConvexCone R G} : C.Salient ↔ ¬C.Flat

theorem ConvexCone.Flat.mono {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] {C₁ C₂ : ConvexCone R G} (h : C₁ ≤ C₂) : C₁.Flat → C₂.Flat

theorem ConvexCone.Salient.anti {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] {C₁ C₂ : ConvexCone R G} (h : C₂ ≤ C₁) : C₁.Salient → C₂.Salient

theorem ConvexCone.Flat.pointed {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] {C : ConvexCone R G} (hC : C.Flat) : C.Pointed

A flat cone is always pointed (contains 0).

theorem ConvexCone.Blunt.salient {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] {C : ConvexCone R G} : C.Blunt → C.Salient

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

def ConvexCone.toPreorder {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) : Preorder G

A pointed convex cone defines a preorder.

Equations

• C.toPreorder h₁ = { le := fun (x y : G) => y - x ∈ C, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

def ConvexCone.toPartialOrder {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient) : PartialOrder G

A pointed and salient cone defines a partial order.

Equations

• C.toPartialOrder h₁ h₂ = { toPreorder := C.toPreorder h₁, le_antisymm := ⋯ }

theorem ConvexCone.to_isOrderedAddMonoid {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient) : have x := C.toPartialOrder h₁ h₂; IsOrderedAddMonoid G

A pointed and salient cone defines an IsOrderedAddMonoid.

@[deprecated ConvexCone.to_isOrderedAddMonoid (since := "2025-06-11")]

theorem ConvexCone.toIsOrderedAddMonoid {R : Type u_2} {G : Type u_3} [Semiring R] [PartialOrder R] [AddCommGroup G] [SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient) : have x := C.toPartialOrder h₁ h₂; IsOrderedAddMonoid G

Alias of ConvexCone.to_isOrderedAddMonoid.

---

A pointed and salient cone defines an IsOrderedAddMonoid.

instance ConvexCone.instZero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : Zero (ConvexCone R M)

Equations

• ConvexCone.instZero = { zero := { carrier := 0, smul_mem' := ⋯, add_mem' := ⋯ } }

@[simp]

theorem ConvexCone.mem_zero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] {x : M} : x ∈ 0 ↔ x = 0

@[simp]

theorem ConvexCone.coe_zero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : ↑0 = 0

theorem ConvexCone.pointed_zero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : Pointed 0

instance ConvexCone.instAdd {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : Add (ConvexCone R M)

Equations

• ConvexCone.instAdd = { add := fun (C₁ C₂ : ConvexCone R M) => { carrier := ↑C₁ + ↑C₂, smul_mem' := ⋯, add_mem' := ⋯ } }

@[simp]

theorem ConvexCone.coe_add {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C₁ C₂ : ConvexCone R M) : ↑(C₁ + C₂) = ↑C₁ + ↑C₂

@[simp]

theorem ConvexCone.mem_add {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] {C₁ C₂ : ConvexCone R M} {x : M} : x ∈ C₁ + C₂ ↔ ∃ y ∈ C₁, ∃ z ∈ C₂, y + z = x

instance ConvexCone.instAddZeroClass {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : AddZeroClass (ConvexCone R M)

Equations

• ConvexCone.instAddZeroClass = { toZero := ConvexCone.instZero, toAdd := ConvexCone.instAdd, zero_add := ⋯, add_zero := ⋯ }

instance ConvexCone.instAddCommSemigroup {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : AddCommSemigroup (ConvexCone R M)

Equations

• ConvexCone.instAddCommSemigroup = { toAdd := ConvexCone.instAdd, add_assoc := ⋯, add_comm := ⋯ }

theorem ConvexCone.mem_hull_of_convex {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} {x : M} (hs : Convex 𝕜 s) : x ∈ hull 𝕜 s ↔ ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s

The cone hull of a convex set is simply the union of the open halflines through that set.

theorem ConvexCone.coe_hull_of_convex {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) : ↑(hull 𝕜 s) = {x : M | ∃ (r : 𝕜), 0 < r ∧ x ∈ r • s}

The cone hull of a convex set is simply the union of the open halflines through that set.

theorem ConvexCone.disjoint_hull_left_of_convex {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {C : ConvexCone 𝕜 M} {s : Set M} (hs : Convex 𝕜 s) : Disjoint (hull 𝕜 s) C ↔ Disjoint s ↑C

theorem ConvexCone.disjoint_hull_right_of_convex {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {C : ConvexCone 𝕜 M} {s : Set M} (hs : Convex 𝕜 s) : Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C) s

Submodules are cones

def Submodule.toConvexCone {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : Submodule R M) : ConvexCone R M

Every submodule is trivially a convex cone.

Equations

• C.toConvexCone = { carrier := ↑C, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem Submodule.coe_toConvexCone {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : Submodule R M) : ↑C.toConvexCone = ↑C

@[simp]

theorem Submodule.mem_toConvexCone {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] {C : Submodule R M} {x : M} : x ∈ C.toConvexCone ↔ x ∈ C

@[simp]

theorem Submodule.toConvexCone_le_toConvexCone {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] {C₁ C₂ : Submodule R M} : C₁.toConvexCone ≤ C₂.toConvexCone ↔ C₁ ≤ C₂

@[deprecated Submodule.toConvexCone_le_toConvexCone (since := "2025-06-11")]

theorem Submodule.toConvexCone_le_iff {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] {C₁ C₂ : Submodule R M} : C₁.toConvexCone ≤ C₂.toConvexCone ↔ C₁ ≤ C₂

Alias of Submodule.toConvexCone_le_toConvexCone.

@[simp]

theorem Submodule.toConvexCone_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : ⊥.toConvexCone = 0

@[simp]

theorem Submodule.toConvexCone_top {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] : ⊤.toConvexCone = ⊤

@[simp]

theorem Submodule.toConvexCone_inf {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C₁ C₂ : Submodule R M) : (C₁ ⊓ C₂).toConvexCone = C₁.toConvexCone ⊓ C₂.toConvexCone

@[simp]

theorem Submodule.pointed_toConvexCone {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : Submodule R M) : C.toConvexCone.Pointed

@[deprecated Submodule.pointed_toConvexCone (since := "2025-06-11")]

theorem Submodule.toConvexCone_pointed {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] (C : Submodule R M) : C.toConvexCone.Pointed

Alias of Submodule.pointed_toConvexCone.

Positive cone of an ordered module

def ConvexCone.positive (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] : ConvexCone R M

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

Equations

• ConvexCone.positive R M = { carrier := Set.Ici 0, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem ConvexCone.mem_positive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] {x : M} : x ∈ positive R M ↔ 0 ≤ x

@[simp]

theorem ConvexCone.coe_positive (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] : ↑(positive R M) = Set.Ici 0

theorem ConvexCone.salient_positive {R : Type u_2} [Semiring R] [PartialOrder R] {G : Type u_7} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Module R G] [PosSMulMono R G] : (positive R G).Salient

The positive cone of an ordered module is always salient.

theorem ConvexCone.pointed_positive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] : (positive R M).Pointed

The positive cone of an ordered module is always pointed.

def ConvexCone.strictlyPositive (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : ConvexCone R M

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

• ConvexCone.strictlyPositive R M = { carrier := Set.Ioi 0, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem ConvexCone.mem_strictlyPositive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] {x : M} : x ∈ strictlyPositive R M ↔ 0 < x

@[simp]

theorem ConvexCone.coe_strictlyPositive (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : ↑(strictlyPositive R M) = Set.Ioi 0

theorem ConvexCone.strictlyPositive_le_positive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : strictlyPositive R M ≤ positive R M

@[deprecated ConvexCone.strictlyPositive_le_positive (since := "2025-05-29")]

theorem ConvexCone.positive_le_strictlyPositive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : strictlyPositive R M ≤ positive R M

Alias of ConvexCone.strictlyPositive_le_positive.

theorem ConvexCone.salient_strictlyPositive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : (strictlyPositive R M).Salient

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

theorem ConvexCone.blunt_strictlyPositive {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulStrictMono R M] : (strictlyPositive R M).Blunt

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

Cone over a convex set

def Convex.toCone {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] (s : Set M) (hs : Convex 𝕜 s) : ConvexCone 𝕜 M

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

Equations

• Convex.toCone s hs = { carrier := ⋃ (c : 𝕜), ⋃ (_ : 0 < c), c • s, smul_mem' := ⋯, add_mem' := ⋯ }

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

theorem Convex.mem_toCone' {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) {x : M} : x ∈ toCone s hs ↔ ∃ (c : 𝕜), 0 < c ∧ c • x ∈ s

theorem Convex.subset_toCone {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) : s ⊆ ↑(toCone s hs)

theorem Convex.toCone_isLeast {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) : IsLeast {t : ConvexCone 𝕜 M | s ⊆ ↑t} (toCone s hs)

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

theorem Convex.toCone_eq_sInf {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s) : toCone s hs = sInf {t : ConvexCone 𝕜 M | s ⊆ ↑t}

theorem convexHull_toCone_isLeast {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] (s : Set M) : IsLeast {t : ConvexCone 𝕜 M | s ⊆ ↑t} (Convex.toCone ((convexHull 𝕜) s) ⋯)

theorem convexHull_toCone_eq_sInf {𝕜 : Type u_1} {M : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup M] [Module 𝕜 M] (s : Set M) : Convex.toCone ((convexHull 𝕜) s) ⋯ = sInf {t : ConvexCone 𝕜 M | s ⊆ ↑t}