Separation Hahn-Banach theorem #

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

In this file we prove the geometric Hahn-Banach theorem. For any two disjoint convex sets, there exists a continuous linear functional separating them, geometrically meaning that we can intercalate a plane between them.

We provide many variations to stricten the result under more assumptions on the convex sets:

geometric_hahn_banach_open: One set is open. Weak separation.
geometric_hahn_banach_open_point, geometric_hahn_banach_point_open: One set is open, the other is a singleton. Weak separation.
geometric_hahn_banach_open_open: Both sets are open. Semistrict separation.
geometric_hahn_banach_compact_closed, geometric_hahn_banach_closed_compact: One set is closed, the other one is compact. Strict separation.
geometric_hahn_banach_point_closed, geometric_hahn_banach_closed_point: One set is closed, the other one is a singleton. Strict separation.
geometric_hahn_banach_point_point: Both sets are singletons. Strict separation.

TODO #

Eidelheit's theorem
convex ℝ s → interior (closure s) ⊆ s

source

theorem separate_convex_open_set {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s : set E} (hs₀ : 0 ∈ s) (hs₁ : convex ℝ s) (hs₂ : is_open s) {x₀ : E} (hx₀ : x₀ ∉ s) :

∃ (f : E →L[ℝ ] ℝ), ⇑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ⇑f x < 1

Given a set s which is a convex neighbourhood of 0 and a point x₀ outside of it, there is a continuous linear functional f separating x₀ and s, in the sense that it sends x₀ to 1 and all of s to values strictly below 1.

source

theorem geometric_hahn_banach_open {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s t : set E} (hs₁ : convex ℝ s) (hs₂ : is_open s) (ht : convex ℝ t) (disj : disjoint s t) :

∃ (f : E →L[ℝ ] ℝ) (u : ℝ), (∀ (a : E), a ∈ s → ⇑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ⇑f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is open, there is a continuous linear functional which separates them.

source

theorem geometric_hahn_banach_open_point {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s : set E} {x : E} (hs₁ : convex ℝ s) (hs₂ : is_open s) (disj : x ∉ s) :

∃ (f : E →L[ℝ ] ℝ), ∀ (a : E), a ∈ s → ⇑f a < ⇑f x

source

theorem geometric_hahn_banach_point_open {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {t : set E} {x : E} (ht₁ : convex ℝ t) (ht₂ : is_open t) (disj : x ∉ t) :

∃ (f : E →L[ℝ ] ℝ), ∀ (b : E), b ∈ t → ⇑f x < ⇑f b

source

theorem geometric_hahn_banach_open_open {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s t : set E} (hs₁ : convex ℝ s) (hs₂ : is_open s) (ht₁ : convex ℝ t) (ht₃ : is_open t) (disj : disjoint s t) :

∃ (f : E →L[ℝ ] ℝ) (u : ℝ), (∀ (a : E), a ∈ s → ⇑f a < u) ∧ ∀ (b : E), b ∈ t → u < ⇑f b

source

theorem geometric_hahn_banach_compact_closed {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s t : set E} [locally_convex_space ℝ E] (hs₁ : convex ℝ s) (hs₂ : is_compact s) (ht₁ : convex ℝ t) (ht₂ : is_closed t) (disj : disjoint s t) :

∃ (f : E →L[ℝ ] ℝ) (u v : ℝ), (∀ (a : E), a ∈ s → ⇑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ⇑f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is compact and t is closed, there is a continuous linear functional which strongly separates them.

source

theorem geometric_hahn_banach_closed_compact {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s t : set E} [locally_convex_space ℝ E] (hs₁ : convex ℝ s) (hs₂ : is_closed s) (ht₁ : convex ℝ t) (ht₂ : is_compact t) (disj : disjoint s t) :

∃ (f : E →L[ℝ ] ℝ) (u v : ℝ), (∀ (a : E), a ∈ s → ⇑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ⇑f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is closed, and t is compact, there is a continuous linear functional which strongly separates them.

source

theorem geometric_hahn_banach_point_closed {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {t : set E} {x : E} [locally_convex_space ℝ E] (ht₁ : convex ℝ t) (ht₂ : is_closed t) (disj : x ∉ t) :

∃ (f : E →L[ℝ ] ℝ) (u : ℝ), ⇑f x < u ∧ ∀ (b : E), b ∈ t → u < ⇑f b

source

theorem geometric_hahn_banach_closed_point {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s : set E} {x : E} [locally_convex_space ℝ E] (hs₁ : convex ℝ s) (hs₂ : is_closed s) (disj : x ∉ s) :

∃ (f : E →L[ℝ ] ℝ) (u : ℝ), (∀ (a : E), a ∈ s → ⇑f a < u) ∧ u < ⇑f x

source

theorem geometric_hahn_banach_point_point {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {x y : E} [locally_convex_space ℝ E] [t1_space E] (hxy : x ≠ y) :

∃ (f : E →L[ℝ ] ℝ), ⇑f x < ⇑f y

source

theorem Inter_halfspaces_eq {E : Type u_2} [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] {s : set E} [locally_convex_space ℝ E] (hs₁ : convex ℝ s) (hs₂ : is_closed s) :

(⋂ (l : E →L[ℝ ] ℝ), {x : E | ∃ (y : E) (H : y ∈ s), ⇑l x ≤ ⇑l y}) = s

A closed convex set is the intersection of the halfspaces containing it.