# Documentation

Mathlib.Analysis.Convex.Cone.Dual

# Convex cones in inner product spaces #

We define Set.innerDualCone 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:

• ConvexCone.innerDualCone_of_innerDualCone_eq_self: The innerDualCone of the innerDualCone of a nonempty, closed, convex cone is itself.

### The dual cone #

def Set.innerDualCone {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 ⟫.

Instances For
@[simp]
theorem mem_innerDualCone {H : Type u_5} [] (y : H) (s : Set H) :
∀ (x : H), x s0 inner x y
@[simp]
theorem innerDualCone_empty {H : Type u_5} [] :
@[simp]
theorem innerDualCone_zero {H : Type u_5} [] :

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

@[simp]
theorem innerDualCone_univ {H : Type u_5} [] :
Set.innerDualCone Set.univ = 0

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

theorem innerDualCone_le_innerDualCone {H : Type u_5} [] (s : Set H) (t : Set H) (h : t s) :
theorem pointed_innerDualCone {H : Type u_5} [] (s : Set H) :
theorem innerDualCone_singleton {H : Type u_5} [] (x : H) :
= ConvexCone.comap (↑() x) ()

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

theorem innerDualCone_union {H : Type u_5} [] (s : Set H) (t : Set H) :
theorem innerDualCone_insert {H : Type u_5} [] (x : H) (s : Set H) :
theorem innerDualCone_iUnion {H : Type u_5} [] {ι : Sort u_6} (f : ιSet H) :
Set.innerDualCone (⋃ (i : ι), f i) = ⨅ (i : ι), Set.innerDualCone (f i)
theorem innerDualCone_sUnion {H : Type u_5} [] (S : Set (Set H)) :
= sInf (Set.innerDualCone '' S)
theorem innerDualCone_eq_iInter_innerDualCone_singleton {H : Type u_5} [] (s : Set H) :
↑() = ⋂ (i : s), ↑()

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

theorem isClosed_innerDualCone {H : Type u_5} [] (s : Set H) :
theorem ConvexCone.pointed_of_nonempty_of_isClosed {H : Type u_5} [] (K : ) (ne : ) (hc : IsClosed K) :
theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem {H : Type u_5} [] [] (K : ) (ne : ) (hc : IsClosed K) {b : H} (disj : ¬b K) :
y, (∀ (x : H), x K0 inner x y) inner y b < 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.

theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self {H : Type u_5} [] [] (K : ) (ne : ) (hc : IsClosed K) :

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