Documentation

Mathlib.Analysis.Convex.Cone.Proper

Proper cones #

We define a proper cone as a closed, pointed cone. Proper cones are used in defining conic programs which generalize linear programs. A linear program is a conic program for the positive cone. We then prove Farkas' lemma for conic programs following the proof in the reference below. Farkas' lemma is equivalent to strong duality. So, once we have the definitions of conic and linear programs, the results from this file can be used to prove duality theorems.

TODO #

The next steps are:

References #

structure ProperCone (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] extends Submodule :
Type u_2

A proper cone is a pointed cone K that is closed. Proper cones have the nice property that they are equal to their double dual, see ProperCone.dual_dual. This makes them useful for defining cone programs and proving duality theorems.

  • carrier : Set E
  • add_mem' : βˆ€ {a b : E}, a ∈ self.carrier β†’ b ∈ self.carrier β†’ a + b ∈ self.carrier
  • zero_mem' : 0 ∈ self.carrier
  • smul_mem' : βˆ€ (c : { c : π•œ // 0 ≀ c }) {x : E}, x ∈ self.carrier β†’ c β€’ x ∈ self.carrier
  • isClosed' : IsClosed self.carrier
Instances For
    theorem ProperCone.isClosed' {π•œ : Type u_1} {E : Type u_2} [OrderedSemiring π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (self : ProperCone π•œ E) :
    IsClosed self.carrier
    @[reducible, inline]
    abbrev ProperCone.toPointedCone {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (C : ProperCone π•œ E) :
    Submodule { c : π•œ // 0 ≀ c } E

    A PointedCone is defined as an alias of submodule. We replicate the abbreviation here and define toPointedCone as an alias of toSubmodule.

    Equations
    • ↑C = C.toSubmodule
    Instances For
      instance ProperCone.instCoePointedCone {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] :
      Coe (ProperCone π•œ E) (PointedCone π•œ E)
      Equations
      • ProperCone.instCoePointedCone = { coe := ProperCone.toPointedCone }
      theorem ProperCone.toPointedCone_injective {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] :
      Function.Injective ProperCone.toPointedCone
      instance ProperCone.instSetLike {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] :
      SetLike (ProperCone π•œ E) E
      Equations
      • ProperCone.instSetLike = { coe := fun (K : ProperCone π•œ E) => K.carrier, coe_injective' := β‹― }
      theorem ProperCone.ext_iff {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {S : ProperCone π•œ E} {T : ProperCone π•œ E} :
      S = T ↔ βˆ€ (x : E), x ∈ S ↔ x ∈ T
      theorem ProperCone.ext {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {S : ProperCone π•œ E} {T : ProperCone π•œ E} (h : βˆ€ (x : E), x ∈ S ↔ x ∈ T) :
      S = T
      @[simp]
      theorem ProperCone.mem_coe {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {x : E} {K : ProperCone π•œ E} :
      x ∈ ↑K ↔ x ∈ K
      instance ProperCone.instZero {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (K : ProperCone π•œ E) :
      Zero β†₯K
      Equations
      theorem ProperCone.nonempty {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (K : ProperCone π•œ E) :
      (↑K).Nonempty
      theorem ProperCone.isClosed {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (K : ProperCone π•œ E) :
      IsClosed ↑K
      def ProperCone.positive (π•œ : Type u_1) (E : Type u_2) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] [TopologicalSpace E] [OrderClosedTopology E] :
      ProperCone π•œ E

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

      Equations
      Instances For
        @[simp]
        theorem ProperCone.mem_positive (π•œ : Type u_2) (E : Type u_1) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] [TopologicalSpace E] [OrderClosedTopology E] {x : E} :
        @[simp]
        theorem ProperCone.coe_positive (π•œ : Type u_2) (E : Type u_1) [OrderedSemiring π•œ] [OrderedAddCommGroup E] [Module π•œ E] [OrderedSMul π•œ E] [TopologicalSpace E] [OrderClosedTopology E] :
        ↑↑(ProperCone.positive π•œ E) = ConvexCone.positive π•œ E
        instance ProperCone.instZero_1 {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module π•œ E] :
        Zero (ProperCone π•œ E)
        Equations
        • ProperCone.instZero_1 = { zero := { toSubmodule := 0, isClosed' := β‹― } }
        instance ProperCone.instInhabited {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module π•œ E] :
        Inhabited (ProperCone π•œ E)
        Equations
        • ProperCone.instInhabited = { default := 0 }
        @[simp]
        theorem ProperCone.mem_zero {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module π•œ E] (x : E) :
        x ∈ 0 ↔ x = 0
        @[simp]
        theorem ProperCone.coe_zero {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module π•œ E] :
        ↑↑0 = 0
        theorem ProperCone.pointed_zero {π•œ : Type u_1} [OrderedSemiring π•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module π•œ E] :
        (↑↑0).Pointed
        theorem ProperCone.pointed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ProperCone ℝ E) :
        (↑↑K).Pointed

        The closure of image of a proper cone under a continuous ℝ-linear map is a proper cone. We use continuous maps here so that the comap of f is also a map between proper cones.

        Equations
        Instances For
          @[simp]
          theorem ProperCone.coe_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E β†’L[ℝ] F) (K : ProperCone ℝ E) :
          ↑(ProperCone.map f K) = (PointedCone.map ↑f ↑K).closure
          @[simp]

          The inner dual cone of a proper cone is a proper cone.

          Equations
          Instances For
            @[simp]
            theorem ProperCone.coe_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ProperCone ℝ E) :
            ↑↑K.dual = (↑K).innerDualCone
            @[simp]
            theorem ProperCone.mem_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : ProperCone ℝ E} {y : E} :
            y ∈ K.dual ↔ βˆ€ ⦃x : E⦄, x ∈ K β†’ 0 ≀ inner x y

            The preimage of a proper cone under a continuous ℝ-linear map is a proper cone.

            Equations
            Instances For
              @[simp]

              The dual of the dual of a proper cone is itself.

              theorem ProperCone.hyperplane_separation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (K : ProperCone ℝ E) {f : E β†’L[ℝ] F} {b : F} :
              b ∈ ProperCone.map f K ↔ βˆ€ (y : F), (ContinuousLinearMap.adjoint f) y ∈ K.dual β†’ 0 ≀ inner y b

              This is a relative version of ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem, which we recover by setting f to be the identity map. This is also a geometric interpretation of the Farkas' lemma stated using proper cones.

              theorem ProperCone.hyperplane_separation_of_nmem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (K : ProperCone ℝ E) {f : E β†’L[ℝ] F} {b : F} (disj : b βˆ‰ ProperCone.map f K) :
              βˆƒ (y : F), (ContinuousLinearMap.adjoint f) y ∈ K.dual ∧ inner y b < 0