Inner dual cone of a set

We define the inner dual cone of a set s in an inner product space to be the proper cone consisting of all points y such that 0 ≤ ⟪x, y⟫ for all x ∈ s.

Main statements

We prove the following theorems:

• ProperCone.innerDual_innerDual: The double inner dual of a proper convex cone is itself.
• ProperCone.hyperplane_separation': This variant of the hyperplane separation theorem states that given a nonempty, closed, convex cone C in a complete, real inner product space E and a point b disjoint from it, there is a vector y which separates b from K in the sense that for all points x in K, 0 ≤ ⟪x, y⟫_ℝ and ⟪y, b⟫_ℝ < 0. This is also a geometric interpretation of the Farkas lemma.

Implementation notes

We do not provide ConvexCone- nor PointedCone-valued versions of ProperCone.innerDual since the inner dual cone of any set is always closed and contains 0, i.e. is a proper cone. Furthermore, the strict version {y | ∀ x ∈ s, 0 < ⟪x, y⟫} is a candidate to the name ConvexCone.innerDual.

def ProperCone.innerDual {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) : ProperCone ℝ E

The dual cone of a set s is the cone consisting of all points y such that for all points x ∈ s we have 0 ≤ ⟪x, y⟫.

Equations

• ProperCone.innerDual s = ProperCone.dual (innerₗ E) s

@[simp]

theorem ProperCone.innerDual_toSubmodule {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s : Set E) : ↑(innerDual s) = PointedCone.dual (innerₗ E) s

@[simp]

theorem ProperCone.mem_innerDual {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {y : E} : y ∈ innerDual s ↔ ∀ ⦃x : E⦄, x ∈ s → 0 ≤ inner ℝ x y

@[simp]

theorem ProperCone.innerDual_empty {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : innerDual ∅ = ⊤

@[simp]

theorem ProperCone.innerDual_zero {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : innerDual 0 = ⊤

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

@[simp]

theorem ProperCone.innerDual_univ {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : innerDual Set.univ = ⊥

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

theorem ProperCone.innerDual_le_innerDual {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s t : Set E} (h : t ⊆ s) : innerDual s ≤ innerDual t

theorem ProperCone.innerDual_singleton {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) : innerDual {x} = comap ((innerSL ℝ) x) (positive ℝ ℝ)

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 ProperCone.innerDual_union {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (s t : Set E) : innerDual (s ∪ t) = innerDual s ⊓ innerDual t

theorem ProperCone.innerDual_insert {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) (s : Set E) : innerDual (insert x s) = innerDual {x} ⊓ innerDual s

theorem ProperCone.innerDual_iUnion {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ι : Sort u_4} (f : ι → Set E) : innerDual (⋃ (i : ι), f i) = ⨅ (i : ι), innerDual (f i)

theorem ProperCone.innerDual_sUnion {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set (Set E)) : innerDual (⋃₀ S) = sInf (innerDual '' S)

Farkas' lemma and double dual of a cone in a Hilbert space

theorem ProperCone.hyperplane_separation' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x₀ : E} (C : ProperCone ℝ E) (hx₀ : x₀ ∉ C) : ∃ (y : E), (∀ x ∈ C, 0 ≤ inner ℝ x y) ∧ inner ℝ x₀ y < 0

Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.

@[simp]

theorem ProperCone.innerDual_innerDual {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : ProperCone ℝ E) : innerDual ↑(innerDual ↑C) = C

The inner dual of inner dual of a proper cone is itself.

theorem ProperCone.relative_hyperplane_separation {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {C : ProperCone ℝ E} {f : E →L[ℝ] F} {b : F} : b ∈ map f C ↔ ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C → 0 ≤ inner ℝ b y

Relative geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.

theorem ProperCone.hyperplane_separation_of_notMem {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F} (disj : b ∉ map f K) : ∃ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑K ∧ inner ℝ b y < 0

theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (K : ConvexCone ℝ H) (ne : (↑K).Nonempty) (hc : IsClosed ↑K) {b : H} (disj : b ∉ K) : ∃ (y : H), (∀ x ∈ K, 0 ≤ 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.