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, ie 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⟫.

@[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

@[deprecated ProperCone.hyperplane_separation_of_notMem (since := "2025-05-24")]

theorem ProperCone.hyperplane_separation_of_nmem {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

Alias of ProperCone.hyperplane_separation_of_notMem.

@[deprecated ProperCone.innerDual (since := "2025-07-06")]

def Set.innerDualCone {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) : ConvexCone ℝ 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 ⟫.

@[deprecated ProperCone.mem_innerDual (since := "2025-07-06")]

theorem mem_innerDualCone {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (y : H) (s : Set H) : y ∈ s.innerDualCone ↔ ∀ x ∈ s, 0 ≤ inner ℝ x y

@[deprecated ProperCone.innerDual_empty (since := "2025-07-06")]

theorem innerDualCone_empty {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : ∅.innerDualCone = ⊤

@[deprecated ProperCone.innerDual_zero (since := "2025-07-06")]

theorem innerDualCone_zero {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Set.innerDualCone 0 = ⊤

@[deprecated ProperCone.innerDual_univ (since := "2025-07-06")]

theorem innerDualCone_univ {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Set.univ.innerDualCone = 0

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

@[deprecated ProperCone.innerDual_le_innerDual (since := "2025-07-06")]

theorem innerDualCone_le_innerDualCone {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {s t : Set H} (h : t ⊆ s) : s.innerDualCone ≤ t.innerDualCone

@[deprecated ProperCone.pointed_toConvexCone (since := "2025-07-06")]

theorem pointed_innerDualCone {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) : s.innerDualCone.Pointed

@[deprecated ProperCone.innerDual_singleton (since := "2025-07-06")]

theorem innerDualCone_singleton {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (x : H) : {x}.innerDualCone = ConvexCone.comap ((innerₛₗ ℝ) x) (ConvexCone.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⟫.

@[deprecated ProperCone.innerDual_union (since := "2025-07-06")]

theorem innerDualCone_union {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s t : Set H) : (s ∪ t).innerDualCone = s.innerDualCone ⊓ t.innerDualCone

@[deprecated ProperCone.innerDual_insert (since := "2025-07-06")]

theorem innerDualCone_insert {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (x : H) (s : Set H) : (insert x s).innerDualCone = {x}.innerDualCone ⊓ s.innerDualCone

@[deprecated ProperCone.innerDual_iUnion (since := "2025-07-06")]

theorem innerDualCone_iUnion {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Sort u_5} (f : ι → Set H) : (⋃ (i : ι), f i).innerDualCone = ⨅ (i : ι), (f i).innerDualCone

@[deprecated ProperCone.innerDual_sUnion (since := "2025-07-06")]

theorem innerDualCone_sUnion {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S : Set (Set H)) : (⋃₀ S).innerDualCone = sInf (Set.innerDualCone '' S)

@[deprecated "No replacement" (since := "2025-07-06")]

theorem innerDualCone_eq_iInter_innerDualCone_singleton {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) : ↑s.innerDualCone = ⋂ (i : ↑s), ↑{↑i}.innerDualCone

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

@[deprecated ProperCone.isClosed (since := "2025-07-06")]

theorem isClosed_innerDualCone {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s : Set H) : IsClosed ↑s.innerDualCone

@[deprecated "Now irrelevant" (since := "2025-07-06")]

theorem PointedCone.toConvexCone_dual {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : PointedCone ℝ H) : ↑(dual (innerₗ H) ↑C) = (↑C).innerDualCone

@[deprecated "Now irrelevant" (since := "2025-07-06")]

theorem ProperCone.coe_dual {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (C : ProperCone ℝ H) : ↑↑(dual (innerₗ H) ↑C) = (↑C).innerDualCone

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.

@[deprecated ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem (since := "2025-05-24")]

theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem {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

Alias of ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem.

---

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

@[deprecated ProperCone.innerDual_innerDual (since := "2025-07-06")]

theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (K : ConvexCone ℝ H) (ne : (↑K).Nonempty) (hc : IsClosed ↑K) : (↑(↑K).innerDualCone).innerDualCone = K

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

@[deprecated ProperCone.innerDual_innerDual (since := "2025-07-06")]

theorem ProperCone.dual_dual {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (K : ProperCone ℝ H) : innerDual ↑(innerDual ↑K) = K

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