Convex cones in inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define set.inner_dual_cone 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:

convex_cone.inner_dual_cone_of_inner_dual_cone_eq_self: The inner_dual_cone of the inner_dual_cone of a nonempty, closed, convex cone is itself.

The dual cone #

source

def set.inner_dual_cone {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s : set H) :

convex_cone ℝ 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.inner_dual_cone = {carrier := {y : H | ∀ (x : H), x ∈ s → 0 ≤ has_inner.inner x y}, smul_mem' := _, add_mem' := _}

source

@[simp]

theorem mem_inner_dual_cone {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (y : H) (s : set H) :

y ∈ s.inner_dual_cone ↔ ∀ (x : H), x ∈ s → 0 ≤ has_inner.inner x y

source

@[simp]

theorem inner_dual_cone_empty {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] :

∅.inner_dual_cone = ⊤

source

@[simp]

theorem inner_dual_cone_zero {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] :

0.inner_dual_cone = ⊤

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

source

@[simp]

theorem inner_dual_cone_univ {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] :

set.univ.inner_dual_cone = 0

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

source

theorem inner_dual_cone_le_inner_dual_cone {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s t : set H) (h : t ⊆ s) :

s.inner_dual_cone ≤ t.inner_dual_cone

source

theorem pointed_inner_dual_cone {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s : set H) :

s.inner_dual_cone.pointed

source

theorem inner_dual_cone_singleton {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (x : H) :

{x}.inner_dual_cone = convex_cone.comap (⇑(innerₛₗ ℝ) x) (convex_cone.positive ℝ ℝ)

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

source

theorem inner_dual_cone_union {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s t : set H) :

(s ∪ t).inner_dual_cone = s.inner_dual_cone ⊓ t.inner_dual_cone

source

theorem inner_dual_cone_insert {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (x : H) (s : set H) :

(has_insert.insert x s).inner_dual_cone = {x}.inner_dual_cone ⊓ s.inner_dual_cone

source

theorem inner_dual_cone_Union {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] {ι : Sort u_1} (f : ι → set H) :

(⋃ (i : ι), f i).inner_dual_cone = ⨅ (i : ι), (f i).inner_dual_cone

source

theorem inner_dual_cone_sUnion {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (S : set (set H)) :

(⋃₀ S).inner_dual_cone = has_Inf.Inf (set.inner_dual_cone '' S)

source

theorem inner_dual_cone_eq_Inter_inner_dual_cone_singleton {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s : set H) :

↑(s.inner_dual_cone) = ⋂ (i : ↥s), ↑({↑i}.inner_dual_cone)

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

source

theorem is_closed_inner_dual_cone {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (s : set H) :

is_closed ↑(s.inner_dual_cone)

source

theorem convex_cone.pointed_of_nonempty_of_is_closed {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] (K : convex_cone ℝ H) (ne : ↑K.nonempty) (hc : is_closed ↑K) :

K.pointed

source

theorem convex_cone.hyperplane_separation_of_nonempty_of_is_closed_of_nmem {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] [complete_space H] (K : convex_cone ℝ H) (ne : ↑K.nonempty) (hc : is_closed ↑K) {b : H} (disj : b ∉ K) :

∃ (y : H), (∀ (x : H), x ∈ K → 0 ≤ has_inner.inner x y) ∧ has_inner.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.

source

theorem convex_cone.inner_dual_cone_of_inner_dual_cone_eq_self {H : Type u_5} [normed_add_comm_group H] [inner_product_space ℝ H] [complete_space H] (K : convex_cone ℝ H) (ne : ↑K.nonempty) (hc : is_closed ↑K) :

↑(↑K.inner_dual_cone).inner_dual_cone = K

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