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
Instances For
@[implicit_reducible]
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
@[implicit_reducible]
instance
ConvexCone.instPartialOrder
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
PartialOrder (ConvexCone R M)
@[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)
:
@[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}
:
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.
Instances For
@[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
@[implicit_reducible]
instance
ConvexCone.instInfSet
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
InfSet (ConvexCone R M)
@[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
@[implicit_reducible]
instance
ConvexCone.instCompleteSemilatticeInf
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
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.
Instances For
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)
:
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}
:
theorem
ConvexCone.gc_hull_coe
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
def
ConvexCone.gi
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
Galois insertion between ConvexCone and SetLike.coe.
Instances For
@[implicit_reducible]
instance
ConvexCone.instBot
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
Bot (ConvexCone R M)
@[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 ∉ ⊥
@[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 = ⊥
@[implicit_reducible]
instance
ConvexCone.instCompleteLattice
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
CompleteLattice (ConvexCone R M)
@[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]
:
@[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}
:
@[implicit_reducible]
instance
ConvexCone.instInhabited
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
:
Inhabited (ConvexCone R M)
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 an R-linear map is a convex cone.
Instances For
@[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)
:
@[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)
:
@[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 an R-linear map is a convex cone.
Instances For
@[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)
:
@[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)
:
@[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)
:
A convex cone is pointed if it includes 0.
Instances For
def
ConvexCone.Blunt
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[SMul R M]
(C : ConvexCone R M)
:
A convex cone is blunt if it doesn't include 0.
Instances For
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}
:
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}
:
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₂)
:
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₁)
:
def
ConvexCone.Flat
{R : Type u_2}
{G : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommGroup G]
[SMul R G]
(C : ConvexCone R G)
:
A convex cone is flat if it contains some nonzero vector x and its opposite -x.
Instances For
def
ConvexCone.Salient
{R : Type u_2}
{G : Type u_3}
[Semiring R]
[PartialOrder R]
[AddCommGroup G]
[SMul R G]
(C : ConvexCone R G)
:
A convex cone is salient if it doesn't include x and -x for any nonzero x.
Instances For
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}
:
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₂)
:
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₁)
:
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}
:
A blunt cone (one not containing 0) is always salient.
@[implicit_reducible]
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.
Instances For
@[implicit_reducible]
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)
:
A pointed and salient cone defines a partial order.
Instances For
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.
@[implicit_reducible]
instance
ConvexCone.instZero
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
Zero (ConvexCone R M)
@[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
@[implicit_reducible]
instance
ConvexCone.instAdd
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
Add (ConvexCone R M)
@[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
@[implicit_reducible]
instance
ConvexCone.instAddZeroClass
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
AddZeroClass (ConvexCone R M)
@[implicit_reducible]
instance
ConvexCone.instAddCommSemigroup
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
AddCommSemigroup (ConvexCone R M)
def
ConvexCone.IsReproducing
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommGroup M]
[Module R M]
(C : ConvexCone R M)
:
A convex cone is reproducing if its set of element differences equals the entire module,
i.e., every element of M can be written as a difference of two elements of C.
See also (IsGenerating).
Instances For
theorem
ConvexCone.IsReproducing.of_univ_subset
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommGroup M]
[Module R M]
{C : ConvexCone R M}
(h : Set.univ ⊆ ↑C - ↑C)
:
A sufficient criterion for a convex cone C to be reproducing is that Set.univ is a subset
of C - C.
theorem
ConvexCone.IsReproducing.sub_eq_univ
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommGroup M]
[Module R M]
{C : ConvexCone R M}
(hC : C.IsReproducing)
:
↑C - ↑C = Set.univ
The set difference of a reproducing cone with itself equals Set.univ.
def
ConvexCone.IsGenerating
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
(C : ConvexCone R M)
:
A convex cone C is generating if its linear span is the entire R-module M.
IsGenerating is equivalent to IsReproducing modulo some conditions.
See IsReproducing.isGenerating and IsGenerating.isReproducing for details.
Instances For
theorem
ConvexCone.IsGenerating.of_top_le_span
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
{C : ConvexCone R M}
(h : ⊤ ≤ Submodule.span R ↑C)
:
A sufficient criteria for a convex cone C to be generating is that top is less than or equal
to the linear span of C.
theorem
ConvexCone.IsGenerating.span_eq_top
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
{C : ConvexCone R M}
(hC : C.IsGenerating)
:
Submodule.span R ↑C = ⊤
The linear span of a generating convex cone equals top.
theorem
ConvexCone.IsGenerating.top_le_span
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
{C : ConvexCone R M}
(hC : C.IsGenerating)
:
Top is less than or equal to the linear span of a generating convex cone.
theorem
ConvexCone.isGenerating_top
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
The whole R-module M (viewed as the top convex cone) is generating.
theorem
ConvexCone.isGenerating_bot_iff
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
:
⊥.IsGenerating ↔ Subsingleton M
The empty convex cone is generating iff the module is a subsingleton.
theorem
ConvexCone.isGenerating_bot
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
[Subsingleton M]
:
In a subsingleton module, the empty convex cone is generating.
theorem
ConvexCone.IsGenerating.mono
{R : Type u_2}
{M : Type u_4}
[Semiring R]
[PartialOrder R]
[AddCommMonoid M]
[Module R M]
{C₁ C₂ : ConvexCone R M}
(h : C₁ ≤ C₂)
(hgen : C₁.IsGenerating)
:
C₂.IsGenerating
A convex cone containing a generating cone is also a generating cone.
theorem
ConvexCone.IsReproducing.isGenerating
{R : Type u_7}
{M : Type u_8}
[Ring R]
[PartialOrder R]
[AddCommGroup M]
[Module R M]
{C : ConvexCone R M}
(h : C.IsReproducing)
:
A reproducing cone is generating.
theorem
ConvexCone.IsGenerating.isReproducing
{R : Type u_7}
{M : Type u_8}
[Ring R]
[LinearOrder R]
[AddLeftStrictMono R]
[AddCommGroup M]
[Nontrivial M]
[Module R M]
{C : ConvexCone R M}
(h : C.IsGenerating)
:
A generating cone is reproducing.
theorem
ConvexCone.isGenerating_iff_isReproducing
{R : Type u_7}
{M : Type u_8}
[Ring R]
[LinearOrder R]
[AddLeftStrictMono R]
[AddCommGroup M]
[Nontrivial M]
[Module R M]
{C : ConvexCone R M}
:
C.IsGenerating ↔ C.IsReproducing
A convex cone is generating iff every element is a difference of cone elements.
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)
:
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)
:
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)
:
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)
:
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.
Instances For
@[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₂
@[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)
:
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.
Instances For
@[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}
:
@[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]
:
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]
:
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]
:
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.
Instances For
@[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]
:
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.
Instances For
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}
:
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}
:
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)
:
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)
:
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}