Documentation

Mathlib.Analysis.Convex.Cone.Basic

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 #

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 π•œ is a predicate on sets, ConvexCone π•œ E is a bundled convex cone.

References #

Definition of ConvexCone and basic properties #

structure ConvexCone (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
Type u_2

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.

  • carrier : Set E

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

  • smul_mem' : βˆ€ ⦃c : π•œβ¦„, 0 < c β†’ βˆ€ ⦃x : E⦄, x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
  • add_mem' : βˆ€ ⦃x : E⦄, x ∈ self.carrier β†’ βˆ€ ⦃y : E⦄, y ∈ self.carrier β†’ x + y ∈ self.carrier
Instances For
    theorem ConvexCone.smul_mem' {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (self : ConvexCone π•œ E) ⦃c : π•œβ¦„ :
    0 < c β†’ βˆ€ ⦃x : E⦄, x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
    theorem ConvexCone.add_mem' {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (self : ConvexCone π•œ E) ⦃x : E⦄ :
    x ∈ self.carrier β†’ βˆ€ ⦃y : E⦄, y ∈ self.carrier β†’ x + y ∈ self.carrier
    instance ConvexCone.instSetLike {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    SetLike (ConvexCone π•œ E) E
    Equations
    • ConvexCone.instSetLike = { coe := ConvexCone.carrier, coe_injective' := β‹― }
    @[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) :
    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.instAddMemClass {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    AddMemClass (ConvexCone π•œ E) E
    Equations
    • β‹― = β‹―
    instance ConvexCone.instInf {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Inf (ConvexCone π•œ E)
    Equations
    • ConvexCone.instInf = { inf := fun (S T : ConvexCone π•œ E) => { carrier := ↑S ∩ ↑T, smul_mem' := β‹―, add_mem' := β‹― } }
    @[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} :
    instance ConvexCone.instInfSet {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    InfSet (ConvexCone π•œ E)
    Equations
    • ConvexCone.instInfSet = { sInf := fun (S : Set (ConvexCone π•œ E)) => { carrier := β‹‚ s ∈ S, ↑s, smul_mem' := β‹―, add_mem' := β‹― } }
    @[simp]
    theorem ConvexCone.coe_sInf {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (S : Set (ConvexCone π•œ E)) :
    ↑(sInf S) = β‹‚ 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 ∈ 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.instBot (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Bot (ConvexCone π•œ E)
    Equations
    theorem ConvexCone.mem_bot (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (x : E) :
    @[simp]
    theorem ConvexCone.coe_bot (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    instance ConvexCone.instTop (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Top (ConvexCone π•œ E)
    Equations
    • ConvexCone.instTop π•œ = { top := { carrier := Set.univ, smul_mem' := β‹―, add_mem' := β‹― } }
    theorem ConvexCone.mem_top (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (x : E) :
    @[simp]
    theorem ConvexCone.coe_top (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    β†‘βŠ€ = Set.univ
    instance ConvexCone.instCompleteLattice (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Equations
    instance ConvexCone.instInhabited (π•œ : Type u_1) {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] :
    Inhabited (ConvexCone π•œ E)
    Equations
    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
    • ConvexCone.map f S = { carrier := ⇑f '' ↑S, smul_mem' := β‹―, add_mem' := β‹― }
    Instances For
      @[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 ∈ 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 (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
      Instances For
        @[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) :
        @[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} :
        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} :
        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) :

        A convex cone is pointed if it includes 0.

        Equations
        Instances For
          def ConvexCone.Blunt {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (S : ConvexCone π•œ E) :

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

          Equations
          • S.Blunt = (0 βˆ‰ S)
          Instances For
            theorem ConvexCone.pointed_iff_not_blunt {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (S : ConvexCone π•œ E) :
            S.Pointed ↔ Β¬S.Blunt
            theorem ConvexCone.blunt_iff_not_pointed {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [SMul π•œ E] (S : ConvexCone π•œ E) :
            S.Blunt ↔ Β¬S.Pointed
            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) :
            S.Pointed β†’ T.Pointed
            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) :
            S.Blunt β†’ T.Blunt
            def ConvexCone.Flat {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] (S : ConvexCone π•œ E) :

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

            Equations
            Instances For
              def ConvexCone.Salient {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] (S : ConvexCone π•œ E) :

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

              Equations
              • S.Salient = βˆ€ x ∈ S, x β‰  0 β†’ -x βˆ‰ S
              Instances For
                theorem ConvexCone.salient_iff_not_flat {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] (S : ConvexCone π•œ E) :
                S.Salient ↔ Β¬S.Flat
                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) :
                S.Flat β†’ T.Flat
                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) :
                S.Salient β†’ T.Salient
                theorem ConvexCone.Flat.pointed {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] {S : ConvexCone π•œ E} (hS : S.Flat) :
                S.Pointed

                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} :
                S.Blunt β†’ S.Salient

                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₁ : S.Pointed) :

                A pointed convex cone defines a preorder.

                Equations
                Instances For
                  def ConvexCone.toPartialOrder {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] (S : ConvexCone π•œ E) (h₁ : S.Pointed) (hβ‚‚ : S.Salient) :

                  A pointed and salient cone defines a partial order.

                  Equations
                  • S.toPartialOrder h₁ hβ‚‚ = let __src := S.toPreorder h₁; PartialOrder.mk β‹―
                  Instances For
                    def ConvexCone.toOrderedAddCommGroup {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommGroup E] [SMul π•œ E] (S : ConvexCone π•œ E) (h₁ : S.Pointed) (hβ‚‚ : S.Salient) :

                    A pointed and salient cone defines an OrderedAddCommGroup.

                    Equations
                    • S.toOrderedAddCommGroup h₁ hβ‚‚ = let __src := S.toPartialOrder h₁ hβ‚‚; let __src_1 := let_fun this := inferInstance; this; OrderedAddCommGroup.mk β‹―
                    Instances For
                      instance ConvexCone.instZero {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                      Zero (ConvexCone π•œ E)
                      Equations
                      • ConvexCone.instZero = { zero := { carrier := 0, smul_mem' := β‹―, add_mem' := β‹― } }
                      @[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] :
                      instance ConvexCone.instAdd {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                      Add (ConvexCone π•œ E)
                      Equations
                      • ConvexCone.instAdd = { add := fun (K₁ Kβ‚‚ : ConvexCone π•œ E) => { carrier := {z : E | βˆƒ x ∈ K₁, βˆƒ y ∈ Kβ‚‚, x + y = z}, smul_mem' := β‹―, add_mem' := β‹― } }
                      @[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 ∈ K₁, βˆƒ y ∈ Kβ‚‚, x + y = a
                      instance ConvexCone.instAddZeroClass {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                      Equations
                      instance ConvexCone.instAddCommSemigroup {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                      Equations

                      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
                      • S.toConvexCone = { carrier := ↑S, smul_mem' := β‹―, add_mem' := β‹― }
                      Instances For
                        @[simp]
                        theorem Submodule.coe_toConvexCone {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (S : Submodule π•œ E) :
                        ↑S.toConvexCone = ↑S
                        @[simp]
                        theorem Submodule.mem_toConvexCone {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] {x : E} {S : Submodule π•œ E} :
                        x ∈ S.toConvexCone ↔ 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} :
                        S.toConvexCone ≀ T.toConvexCone ↔ S ≀ T
                        @[simp]
                        theorem Submodule.toConvexCone_bot {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                        βŠ₯.toConvexCone = 0
                        @[simp]
                        theorem Submodule.toConvexCone_top {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] :
                        ⊀.toConvexCone = ⊀
                        @[simp]
                        theorem Submodule.toConvexCone_inf {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (S : Submodule π•œ E) (T : Submodule π•œ E) :
                        (S βŠ“ T).toConvexCone = S.toConvexCone βŠ“ T.toConvexCone
                        @[simp]
                        theorem Submodule.pointed_toConvexCone {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [Module π•œ E] (S : Submodule π•œ E) :
                        S.toConvexCone.Pointed

                        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
                        Instances For
                          @[simp]
                          theorem ConvexCone.mem_positive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] {x : E} :
                          @[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.positive π•œ E).Salient

                          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.positive π•œ E).Pointed

                          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
                          Instances For
                            @[simp]
                            theorem ConvexCone.mem_strictlyPositive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] {x : E} :
                            @[simp]
                            theorem ConvexCone.coe_strictlyPositive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] :
                            theorem ConvexCone.positive_le_strictlyPositive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] :
                            theorem ConvexCone.salient_strictlyPositive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] :
                            (ConvexCone.strictlyPositive π•œ E).Salient

                            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.strictlyPositive π•œ E).Blunt

                            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
                            • Convex.toCone s hs = { carrier := ⋃ (c : π•œ), ⋃ (_ : 0 < c), c β€’ s, smul_mem' := β‹―, add_mem' := β‹― }
                            Instances For
                              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 ∈ 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 : ConvexCone π•œ E | 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 : ConvexCone π•œ E | s βŠ† ↑t}
                              theorem convexHull_toCone_isLeast {π•œ : Type u_1} {E : Type u_2} [LinearOrderedField π•œ] [AddCommGroup E] [Module π•œ E] (s : Set E) :
                              IsLeast {t : ConvexCone π•œ E | s βŠ† ↑t} (Convex.toCone ((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) β‹― = sInf {t : ConvexCone π•œ E | s βŠ† ↑t}