Documentation

Mathlib.Analysis.Convex.Cone.InnerDual

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:

The dual cone #

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_innerDualCone {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace H] (y : H) (s : Set H) :
y s.innerDualCone xs, 0 inner x y
@[simp]

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

@[simp]

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

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_iUnion {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace H] {ι : Sort u_2} (f : ιSet H) :
(⋃ (i : ι), f i).innerDualCone = ⨅ (i : ι), (f i).innerDualCone

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

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 : bK) :
∃ (y : H), (∀ xK, 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.

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