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:

• Add convex_cone_class that extends set_like and replace the below instance
• Define primal and dual cone programs and prove weak duality.
• Prove regular and strong duality for cone programs using Farkas' lemma (see reference).
• Define linear programs and prove LP duality as a special case of cone duality.
• Find a better reference (textbook instead of lecture notes).

References

• [B. Gartner and J. Matousek, Cone Programming][gartnerMatousek]

@[reducible, inline]

abbrev ProperCone (R : Type u_1) (E : Type u_2) [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] : Type u_2

A proper cone is a pointed cone C 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.

Equations

• ProperCone R E = ClosedSubmodule { r : R // 0 ≤ r } E

@[reducible, inline]

abbrev ProperCone.toPointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : PointedCone R E

Any proper cone can be seen as a pointed cone.

This is an alias of ClosedSubmodule.toSubmodule for convenience and discoverability.

Equations

• ↑C = ↑C

instance ProperCone.instCoePointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] : Coe (ProperCone R E) (PointedCone R E)

Equations

• ProperCone.instCoePointedCone = { coe := ProperCone.toPointedCone }

theorem ProperCone.toPointedCone_injective {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] : Function.Injective toPointedCone

instance ProperCone.instSetLike {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] : SetLike (ProperCone R E) E

Equations

• ProperCone.instSetLike = { coe := fun (C : ProperCone R E) => (↑C).carrier, coe_injective' := ⋯ }

theorem ProperCone.ext {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {C₁ C₂ : ProperCone R E} (h : ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂

theorem ProperCone.ext_iff {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {C₁ C₂ : ProperCone R E} : C₁ = C₂ ↔ ∀ (x : E), x ∈ C₁ ↔ x ∈ C₂

@[simp]

theorem ProperCone.mem_toPointedCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {C : ProperCone R E} {x : E} : x ∈ ↑C ↔ x ∈ C

@[deprecated ProperCone.mem_toPointedCone (since := "2025-06-11")]

theorem ProperCone.mem_coe {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {C : ProperCone R E} {x : E} : x ∈ ↑C ↔ x ∈ C

Alias of ProperCone.mem_toPointedCone.

theorem ProperCone.pointed_toConvexCone {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : (↑↑C).Pointed

@[deprecated ProperCone.pointed_toConvexCone (since := "2025-06-11")]

theorem ProperCone.pointed {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : (↑↑C).Pointed

Alias of ProperCone.pointed_toConvexCone.

theorem ProperCone.nonempty {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : (↑C).Nonempty

theorem ProperCone.isClosed {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : IsClosed ↑C

theorem ProperCone.smul_mem {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {r : R} {x : E} (C : ProperCone R E) (hx : x ∈ C) (hr : 0 ≤ r) : r • x ∈ C

theorem ProperCone.mem_bot {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {x : E} [T1Space E] : x ∈ ⊥ ↔ x = 0

@[simp]

theorem ProperCone.coe_bot {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [T1Space E] : ↑⊥ = {0}

@[simp]

theorem ProperCone.toPointedCone_bot {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [T1Space E] : ↑⊥ = ⊥

@[deprecated ProperCone.mem_bot (since := "2025-06-11")]

theorem ProperCone.mem_zero {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] {x : E} [T1Space E] : x ∈ ⊥ ↔ x = 0

Alias of ProperCone.mem_bot.

@[deprecated ProperCone.coe_bot (since := "2025-06-11")]

theorem ProperCone.coe_zero {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [T1Space E] : ↑⊥ = {0}

Alias of ProperCone.coe_bot.

@[deprecated ProperCone.pointed_toConvexCone (since := "2025-06-11")]

theorem ProperCone.pointed_zero {R : Type u_1} {E : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] (C : ProperCone R E) : (↑↑C).Pointed

Alias of ProperCone.pointed_toConvexCone.

@[reducible, inline]

abbrev ProperCone.comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] (f : E →L[R] F) (C : ProperCone R F) : ProperCone R E

The closure of image of a proper cone under a R-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

• ProperCone.comap f C = ClosedSubmodule.comap (ContinuousLinearMap.restrictScalars { r : R // 0 ≤ r } f) C

@[simp]

theorem ProperCone.comap_id {R : Type u_1} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid F] [TopologicalSpace F] [Module R F] (C : ProperCone R F) : comap (ContinuousLinearMap.id R F) C = C

@[simp]

theorem ProperCone.coe_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] (f : E →L[R] F) (C : ProperCone R F) : ↑(comap f C) = ⇑f ⁻¹' ↑C

theorem ProperCone.comap_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] (g : F →L[R] G) (f : E →L[R] F) (C : ProperCone R G) : comap f (comap g C) = comap (g.comp f) C

theorem ProperCone.mem_comap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] {x : E} {C : ProperCone R F} {f : E →L[R] F} : x ∈ comap f C ↔ f x ∈ C

@[reducible, inline]

abbrev ProperCone.map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [ContinuousAdd F] [ContinuousConstSMul R F] (f : E →L[R] F) (C : ProperCone R E) : ProperCone R F

The closure of image of a proper cone under a linear map is a proper cone.

We use continuous maps here to match ProperCone.comap.

Equations

• ProperCone.map f C = ClosedSubmodule.map (ContinuousLinearMap.restrictScalars { r : R // 0 ≤ r } f) C

@[simp]

theorem ProperCone.map_id {R : Type u_1} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [ContinuousAdd F] [ContinuousConstSMul R F] (C : ProperCone R F) : map (ContinuousLinearMap.id R F) C = C

@[simp]

theorem ProperCone.coe_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [ContinuousAdd F] [ContinuousConstSMul R F] (f : E →L[R] F) (C : ProperCone R E) : ↑(map f C) = (PointedCone.map ↑f ↑C).closure

@[simp]

theorem ProperCone.mem_map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [ContinuousAdd F] [ContinuousConstSMul R F] {f : E →L[R] F} {C : ProperCone R E} {y : F} : y ∈ map f C ↔ y ∈ (PointedCone.map ↑f ↑C).closure

def ProperCone.positive (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] (E : Type u_5) [AddCommGroup E] [TopologicalSpace E] [Module R E] [PartialOrder E] [IsOrderedAddMonoid E] [OrderedSMul R E] [OrderClosedTopology E] : ProperCone R E

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

Equations

• ProperCone.positive R E = { toSubmodule := PointedCone.positive R E, isClosed' := ⋯ }

@[simp]

theorem ProperCone.coe_positive (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] (E : Type u_5) [AddCommGroup E] [TopologicalSpace E] [Module R E] [PartialOrder E] [IsOrderedAddMonoid E] [OrderedSMul R E] [OrderClosedTopology E] : ↑(positive R E) = Set.Ici 0

@[simp]

theorem ProperCone.mem_positive {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {E : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module R E] [PartialOrder E] [IsOrderedAddMonoid E] [OrderedSMul R E] [OrderClosedTopology E] {x : E} : x ∈ positive R E ↔ 0 ≤ x

@[simp]

theorem ProperCone.toPointedCone_positive {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {E : Type u_5} [AddCommGroup E] [TopologicalSpace E] [Module R E] [PartialOrder E] [IsOrderedAddMonoid E] [OrderedSMul R E] [OrderClosedTopology E] : ↑(positive R E) = PointedCone.positive R E