analysis.convex.cone.proper

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 #

In the next few PRs (already sorry-free), we will add the definition and prove several properties of proper cones and finally prove the cone version of Farkas' lemma (2.3.4 in the reference).

The next steps are:

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.

References #

B. Gartner and J. Matousek, Cone Programming

source

@[protected]

def convex_cone.closure {E : Type u_1} [add_comm_monoid E] [has_smul ℝ E] [topological_space E] [has_continuous_const_smul ℝ E] [has_continuous_add E] (K : convex_cone ℝ E) :

convex_cone ℝ E

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

Equations

K.closure = {carrier := closure ↑K, smul_mem' := _, add_mem' := _}

source

@[simp, norm_cast]

theorem convex_cone.coe_closure {E : Type u_1} [add_comm_monoid E] [has_smul ℝ E] [topological_space E] [has_continuous_const_smul ℝ E] [has_continuous_add E] (K : convex_cone ℝ E) :

↑(K.closure) = closure ↑K

source

@[protected]

theorem convex_cone.mem_closure {E : Type u_1} [add_comm_monoid E] [has_smul ℝ E] [topological_space E] [has_continuous_const_smul ℝ E] [has_continuous_add E] {K : convex_cone ℝ E} {a : E} :

a ∈ K.closure ↔ a ∈ closure ↑K