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 #
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.
Instances For
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
Equations
- ProperCone.instCoePointedCone = { coe := ProperCone.toPointedCone }
Equations
- ProperCone.instSetLike = { coe := fun (K : ProperCone π E) => K.carrier, coe_injective' := β― }
Equations
- K.instZero = PointedCone.instZero K.toSubmodule
The positive cone is the proper cone formed by the set of nonnegative elements in an ordered module.
Equations
- ProperCone.positive π E = { toSubmodule := PointedCone.positive π E, isClosed' := β― }
Instances For
Equations
- ProperCone.instZero_1 = { zero := { toSubmodule := 0, isClosed' := β― } }
Equations
- ProperCone.instInhabited = { default := 0 }
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
- ProperCone.map f K = { toSubmodule := (PointedCone.map βf βK).closure, isClosed' := β― }
Instances For
The inner dual cone of a proper cone is a proper cone.
Equations
- K.dual = { toSubmodule := PointedCone.dual βK, isClosed' := β― }
Instances For
The preimage of a proper cone under a continuous β
-linear map is a proper cone.
Equations
- ProperCone.comap f S = { toSubmodule := PointedCone.comap βf βS, isClosed' := β― }
Instances For
The dual of the dual of a proper cone is itself.
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.