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

source
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

Instances For

source
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' := ⋯ }

source
@[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
source
@[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
source
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 `ConvexCone`s are equal if they have the same elements.

source
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₂
source
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
source
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
source
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
source
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' := ⋯ }

Instances For

source
@[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
source
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
source
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' := ⋯ } }

source
@[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
source
@[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
source
@[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)
source
@[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
source
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 := ⋯ }

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

Instances For

source
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)
source
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
source
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
source
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
source
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 := ⋯ }

Instances For

source
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' := ⋯ } }

source
@[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 ∉ ⊥
source
@[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
source
@[simp]
theorem ConvexCone.coe_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] :
↑⊥ = ∅
source
@[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 = ⊥
source
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.

source
@[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₂
source
@[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₂
source
@[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 ∈ ⊤
source
@[simp]
theorem ConvexCone.coe_top {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [SMul R M] :
↑⊤ = Set.univ
source
@[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₂
source
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 := ⊥ }

source
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
source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
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
source
@[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
source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
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
source
@[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
source
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 #

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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
source
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
source
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
source
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`).

source
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.

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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`.

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

source
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' := ⋯ } }

source
@[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
source
@[simp]
theorem ConvexCone.coe_zero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] :
↑0 = 0
source
theorem ConvexCone.pointed_zero {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] :
Pointed 0
source
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' := ⋯ } }

source
@[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₂
source
@[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
source
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 := ⋯ }

source
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 := ⋯ }

source
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.

source
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.

source
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
source
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 #

source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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₂
source
@[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`.

source
@[simp]
theorem Submodule.toConvexCone_bot {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] :
⊥.toConvexCone = 0
source
@[simp]
theorem Submodule.toConvexCone_top {R : Type u_2} {M : Type u_4} [Semiring R] [PartialOrder R] [AddCommMonoid M] [Module R M] :
⊤.toConvexCone = ⊤
source
@[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
source
@[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
source
@[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 #

source
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' := ⋯ }

Instances For

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

source
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.

source
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' := ⋯ }

Instances For

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

source
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.

source
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 #

source
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' := ⋯ }

Instances For

source
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
source
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
source
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)
source
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`.

source
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}
source
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) ⋯)
source
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}