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.
• ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem: This variant of the hyperplane separation theorem states that given a nonempty, closed, convex cone K in a complete, real inner product space H 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.

The dual cone

def Set.innerDualCone {H : Type u_1} [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 ⟫.

Equations

• s.innerDualCone = { carrier := {y : H | ∀ x ∈ s, 0 ≤ inner ℝ x y}, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

theorem innerDualCone_singleton {H : Type u_1} [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⟫.

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

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

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

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

theorem innerDualCone_eq_iInter_innerDualCone_singleton {H : Type u_1} [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.

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

theorem ConvexCone.pointed_of_nonempty_of_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ConvexCone ℝ H) (ne : (↑K).Nonempty) (hc : IsClosed ↑K) : K.Pointed

def PointedCone.dual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : PointedCone ℝ H) : PointedCone ℝ H

The inner dual cone of a pointed cone is a pointed cone.

Equations

• C.dual = ConvexCone.toPointedCone ⋯

@[simp]

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

@[simp]

theorem PointedCone.mem_dual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {C : PointedCone ℝ H} {y : H} : y ∈ C.dual ↔ ∀ ⦃x : H⦄, x ∈ C → 0 ≤ inner ℝ x y

def ProperCone.dual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (C : ProperCone ℝ H) : ProperCone ℝ H

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

Equations

• C.dual = { toSubmodule := (↑C).dual, isClosed' := ⋯ }

@[simp]

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

@[simp]

theorem ProperCone.mem_dual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {C : ProperCone ℝ H} {y : H} : y ∈ C.dual ↔ ∀ ⦃x : H⦄, x ∈ C → 0 ≤ inner ℝ x y

theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem {H : Type u_1} [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_1} [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.

theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self {H : Type u_1} [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.

@[simp]

theorem ProperCone.dual_dual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (K : ProperCone ℝ H) : K.dual.dual = K

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

theorem ProperCone.hyperplane_separation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (K : ProperCone ℝ H) {f : H →L[ℝ] F} {b : F} : b ∈ map f K ↔ ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ K.dual → 0 ≤ inner ℝ y b

This is a relative version of ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_notMem, which we recover by setting f to be the identity map. This is also a geometric interpretation of the Farkas' lemma stated using proper cones.

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

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

theorem ProperCone.hyperplane_separation_of_nmem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (K : ProperCone ℝ H) {f : H →L[ℝ] F} {b : F} (disj : b ∉ map f K) : ∃ (y : F), (ContinuousLinearMap.adjoint f) y ∈ K.dual ∧ inner ℝ y b < 0

Alias of ProperCone.hyperplane_separation_of_notMem.