Proper cones #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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:
- Add convex_cone_class that extends set_like and replace the below instance
- Define the positive cone as a proper cone.
- 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).
- Show submodules are (proper) cones.
References #
@[protected]
def
convex_cone.closure
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_continuous_add E]
[has_smul 𝕜 E]
[has_continuous_const_smul 𝕜 E]
(K : convex_cone 𝕜 E) :
convex_cone 𝕜 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.
@[simp, norm_cast]
theorem
convex_cone.coe_closure
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_continuous_add E]
[has_smul 𝕜 E]
[has_continuous_const_smul 𝕜 E]
(K : convex_cone 𝕜 E) :
@[protected, simp]
theorem
convex_cone.mem_closure
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_continuous_add E]
[has_smul 𝕜 E]
[has_continuous_const_smul 𝕜 E]
{K : convex_cone 𝕜 E}
{a : E} :
@[simp]
theorem
convex_cone.closure_eq
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_continuous_add E]
[has_smul 𝕜 E]
[has_continuous_const_smul 𝕜 E]
{K L : convex_cone 𝕜 E} :
structure
proper_cone
(𝕜 : Type u_1)
(E : Type u_2)
[ordered_semiring 𝕜]
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E] :
Type u_2
- to_convex_cone : convex_cone 𝕜 E
- nonempty' : self.to_convex_cone.carrier.nonempty
- is_closed' : is_closed self.to_convex_cone.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 proper_cone
- proper_cone.has_sizeof_inst
- proper_cone.convex_cone.has_coe
- proper_cone.set_like
- proper_cone.has_zero
- proper_cone.inhabited
@[protected, instance]
def
proper_cone.convex_cone.has_coe
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E] :
has_coe (proper_cone 𝕜 E) (convex_cone 𝕜 E)
Equations
- proper_cone.convex_cone.has_coe = {coe := λ (K : proper_cone 𝕜 E), K.to_convex_cone}
@[simp]
theorem
proper_cone.to_convex_cone_eq_coe
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E]
(K : proper_cone 𝕜 E) :
K.to_convex_cone = ↑K
theorem
proper_cone.ext'
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E] :
@[protected, instance]
def
proper_cone.set_like
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E] :
set_like (proper_cone 𝕜 E) E
Equations
- proper_cone.set_like = {coe := λ (K : proper_cone 𝕜 E), K.to_convex_cone.carrier, coe_injective' := _}
@[ext]
theorem
proper_cone.ext
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E]
{S T : proper_cone 𝕜 E}
(h : ∀ (x : E), x ∈ S ↔ x ∈ T) :
S = T
@[simp]
theorem
proper_cone.mem_coe
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E]
{x : E}
{K : proper_cone 𝕜 E} :
@[protected]
theorem
proper_cone.nonempty
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E]
(K : proper_cone 𝕜 E) :
@[protected]
theorem
proper_cone.is_closed
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[has_smul 𝕜 E]
(K : proper_cone 𝕜 E) :
@[protected, instance]
def
proper_cone.has_zero
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[t1_space E]
[module 𝕜 E] :
has_zero (proper_cone 𝕜 E)
Equations
- proper_cone.has_zero = {zero := {to_convex_cone := 0, nonempty' := _, is_closed' := _}}
@[protected, instance]
def
proper_cone.inhabited
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[t1_space E]
[module 𝕜 E] :
inhabited (proper_cone 𝕜 E)
Equations
- proper_cone.inhabited = {default := 0}
@[simp]
theorem
proper_cone.mem_zero
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[t1_space E]
[module 𝕜 E]
(x : E) :
@[simp, norm_cast]
theorem
proper_cone.coe_zero
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[t1_space E]
[module 𝕜 E] :
theorem
proper_cone.pointed_zero
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{E : Type u_2}
[add_comm_monoid E]
[topological_space E]
[t1_space E]
[module 𝕜 E] :
@[protected]
theorem
proper_cone.pointed
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
(K : proper_cone ℝ E) :
noncomputable
def
proper_cone.map
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
(f : E →L[ℝ] F)
(K : proper_cone ℝ E) :
proper_cone ℝ F
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
- proper_cone.map f K = {to_convex_cone := (convex_cone.map ↑f ↑K).closure, nonempty' := _, is_closed' := _}
@[simp, norm_cast]
theorem
proper_cone.coe_map
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
(f : E →L[ℝ] F)
(K : proper_cone ℝ E) :
↑(proper_cone.map f K) = (convex_cone.map ↑f ↑K).closure
@[simp]
theorem
proper_cone.mem_map
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
{f : E →L[ℝ] F}
{K : proper_cone ℝ E}
{y : F} :
y ∈ proper_cone.map f K ↔ y ∈ (convex_cone.map ↑f ↑K).closure
@[simp]
theorem
proper_cone.map_id
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
(K : proper_cone ℝ E) :
proper_cone.map (continuous_linear_map.id ℝ E) K = K
def
proper_cone.dual
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
(K : proper_cone ℝ E) :
proper_cone ℝ E
The inner dual cone of a proper cone is a proper cone.
Equations
- K.dual = {to_convex_cone := ↑K.inner_dual_cone, nonempty' := _, is_closed' := _}
@[simp, norm_cast]
theorem
proper_cone.coe_dual
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
(K : proper_cone ℝ E) :
↑(K.dual) = ↑K.inner_dual_cone
@[simp]
theorem
proper_cone.mem_dual
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{K : proper_cone ℝ E}
{y : E} :
noncomputable
def
proper_cone.comap
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
(f : E →L[ℝ] F)
(S : proper_cone ℝ F) :
proper_cone ℝ E
The preimage of a proper cone under a continuous ℝ-linear map is a proper cone.
Equations
- proper_cone.comap f S = {to_convex_cone := convex_cone.comap ↑f ↑S, nonempty' := _, is_closed' := _}
@[simp]
theorem
proper_cone.coe_comap
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
(f : E →L[ℝ] F)
(S : proper_cone ℝ F) :
@[simp]
theorem
proper_cone.comap_id
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
(S : convex_cone ℝ E) :
theorem
proper_cone.comap_comap
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
{G : Type u_3}
[normed_add_comm_group G]
[inner_product_space ℝ G]
(g : F →L[ℝ] G)
(f : E →L[ℝ] F)
(S : proper_cone ℝ G) :
proper_cone.comap f (proper_cone.comap g S) = proper_cone.comap (g.comp f) S
@[simp]
theorem
proper_cone.mem_comap
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
{f : E →L[ℝ] F}
{S : proper_cone ℝ F}
{x : E} :
x ∈ proper_cone.comap f S ↔ ⇑f x ∈ S
@[simp]
theorem
proper_cone.dual_dual
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
[complete_space E]
(K : proper_cone ℝ E) :
The dual of the dual of a proper cone is itself.
theorem
proper_cone.hyperplane_separation
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
[complete_space E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
[complete_space F]
(K : proper_cone ℝ E)
{f : E →L[ℝ] F}
{b : F} :
b ∈ proper_cone.map f K ↔ ∀ (y : F), ⇑(⇑continuous_linear_map.adjoint f) y ∈ K.dual → 0 ≤ has_inner.inner y b
This is a relative version of
convex_cone.hyperplane_separation_of_nonempty_of_is_closed_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
proper_cone.hyperplane_separation_of_nmem
{E : Type u_1}
[normed_add_comm_group E]
[inner_product_space ℝ E]
[complete_space E]
{F : Type u_2}
[normed_add_comm_group F]
[inner_product_space ℝ F]
[complete_space F]
(K : proper_cone ℝ E)
{f : E →L[ℝ] F}
{b : F}
(disj : b ∉ proper_cone.map f K) :
∃ (y : F), ⇑(⇑continuous_linear_map.adjoint f) y ∈ K.dual ∧ has_inner.inner y b < 0