# mathlib3documentation

analysis.convex.cone.dual

# Convex cones in inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define set.inner_dual_cone to be the cone consisting of all points y such that for all points x in a given set 0 ≤ ⟪ x, y ⟫.

## Main statements #

We prove the following theorems:

• convex_cone.inner_dual_cone_of_inner_dual_cone_eq_self: The inner_dual_cone of the inner_dual_cone of a nonempty, closed, convex cone is itself.

### The dual cone #

def set.inner_dual_cone {H : Type u_5} (s : set H) :

The dual cone is the cone consisting of all points y such that for all points x in a given set 0 ≤ ⟪ x, y ⟫.

Equations
@[simp]
theorem mem_inner_dual_cone {H : Type u_5} (y : H) (s : set H) :
(x : H), x s 0
@[simp]
theorem inner_dual_cone_empty {H : Type u_5}  :
@[simp]
theorem inner_dual_cone_zero {H : Type u_5}  :

Dual cone of the convex cone {0} is the total space.

@[simp]
theorem inner_dual_cone_univ {H : Type u_5}  :

Dual cone of the total space is the convex cone {0}.

theorem inner_dual_cone_le_inner_dual_cone {H : Type u_5} (s t : set H) (h : t s) :
theorem pointed_inner_dual_cone {H : Type u_5} (s : set H) :

The inner dual cone of a singleton is given by the preimage of the positive cone under the linear map λ y, ⟪x, y⟫.

theorem inner_dual_cone_union {H : Type u_5} (s t : set H) :
theorem inner_dual_cone_insert {H : Type u_5} (x : H) (s : set H) :
theorem inner_dual_cone_Union {H : Type u_5} {ι : Sort u_1} (f : ι set H) :
( (i : ι), f i).inner_dual_cone = (i : ι), (f i).inner_dual_cone
theorem inner_dual_cone_sUnion {H : Type u_5} (S : set (set H)) :

The dual cone of s equals the intersection of dual cones of the points in s.

theorem is_closed_inner_dual_cone {H : Type u_5} (s : set H) :
theorem convex_cone.pointed_of_nonempty_of_is_closed {H : Type u_5} (K : H) (ne : K.nonempty) (hc : is_closed K) :
theorem convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem {H : Type u_5} (K : H) (ne : K.nonempty) (hc : is_closed K) {b : H} (disj : b K) :
(y : H), ( (x : H), x K 0 y) < 0

This is a stronger version of the Hahn-Banach separation theorem for closed convex cones. This is also the geometric interpretation of Farkas' lemma.

The inner dual of inner dual of a non-empty, closed convex cone is itself.