Documentation

Mathlib.Analysis.Convex.Cone.Proper

Proper cones #

We define a proper cone as a nonempty, closed, convex 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 have the definitions of conic programs and linear programs, the results from this file can be used to prove duality theorems.

TODO #

The next steps are:

References #

def ConvexCone.closure {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul ๐•œ E] [ContinuousConstSMul ๐•œ E] (K : ConvexCone ๐•œ E) :
ConvexCone ๐•œ E

The closure of a convex cone inside a topological space as a convex cone. This construction is mainly used for defining maps between proper cones.

Instances For
    @[simp]
    theorem ConvexCone.coe_closure {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul ๐•œ E] [ContinuousConstSMul ๐•œ E] (K : ConvexCone ๐•œ E) :
    โ†‘(ConvexCone.closure K) = closure โ†‘K
    @[simp]
    theorem ConvexCone.mem_closure {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul ๐•œ E] [ContinuousConstSMul ๐•œ E] {K : ConvexCone ๐•œ E} {a : E} :
    @[simp]
    theorem ConvexCone.closure_eq {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [ContinuousAdd E] [SMul ๐•œ E] [ContinuousConstSMul ๐•œ E] {K : ConvexCone ๐•œ E} {L : ConvexCone ๐•œ E} :
    ConvexCone.closure K = L โ†” closure โ†‘K = โ†‘L
    structure ProperCone (๐•œ : Type u_1) (E : Type u_2) [OrderedSemiring ๐•œ] [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ E] extends ConvexCone :
    Type u_2
    • carrier : Set E
    • smul_mem' : โˆ€ โฆƒc : ๐•œโฆ„, 0 < c โ†’ โˆ€ โฆƒx : Eโฆ„, x โˆˆ s.carrier โ†’ c โ€ข x โˆˆ s.carrier
    • add_mem' : โˆ€ โฆƒx : Eโฆ„, x โˆˆ s.carrier โ†’ โˆ€ โฆƒy : Eโฆ„, y โˆˆ s.carrier โ†’ x + y โˆˆ s.carrier
    • nonempty' : Set.Nonempty s.carrier
    • is_closed' : IsClosed s.carrier

    A proper cone is a convex cone K that is nonempty and closed. Proper cones have the nice property that the dual of the dual of a proper cone is itself. This makes them useful for defining cone programs and proving duality theorems.

    Instances For
      instance ProperCone.instCoeProperConeConvexCone {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ E] :
      Coe (ProperCone ๐•œ E) (ConvexCone ๐•œ E)
      theorem ProperCone.ext' {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ E] :
      Function.Injective ProperCone.toConvexCone
      instance ProperCone.instSetLikeProperCone {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ E] :
      SetLike (ProperCone ๐•œ E) E
      theorem ProperCone.ext {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ 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] [SMul ๐•œ E] {x : E} {K : ProperCone ๐•œ E} :
      x โˆˆ K.toConvexCone โ†” x โˆˆ K
      theorem ProperCone.nonempty {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ E] (K : ProperCone ๐•œ E) :
      Set.Nonempty โ†‘K
      theorem ProperCone.isClosed {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [SMul ๐•œ 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.

      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).toConvexCone = ConvexCone.positive ๐•œ E
        @[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.toConvexCone = 0
        theorem ProperCone.pointed_zero {๐•œ : Type u_1} [OrderedSemiring ๐•œ] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module ๐•œ E] :
        ConvexCone.Pointed 0.toConvexCone

        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.

        Instances For
          @[simp]

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

          Instances For
            @[simp]
            theorem ProperCone.mem_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace โ„ E] {K : ProperCone โ„ E} {y : E} :
            y โˆˆ ProperCone.dual K โ†” โˆ€ โฆƒx : Eโฆ„, x โˆˆ K โ†’ 0 โ‰ค inner x y

            The preimage of a proper cone under a continuous โ„-linear map is a proper cone.

            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 โˆˆ ProperCone.dual K โ†’ 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 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, โ†‘(โ†‘ContinuousLinearMap.adjoint f) y โˆˆ ProperCone.dual K โˆง inner y b < 0