Documentation

Mathlib.Analysis.NormedSpace.HahnBanach.Separation

Separation Hahn-Banach theorem #

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:

TODO #

theorem separate_convex_open_set {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} (hs₀ : 0 s) (hs₁ : Convex s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀s) :
∃ (f : E →L[] ), f x₀ = 1 xs, 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.

theorem geometric_hahn_banach_open {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {t : Set E} (hs₁ : Convex s) (hs₂ : IsOpen s) (ht : Convex t) (disj : Disjoint s t) :
∃ (f : E →L[] ) (u : ), (as, f a < u) bt, 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.

theorem geometric_hahn_banach_open_point {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {x : E} (hs₁ : Convex s) (hs₂ : IsOpen s) (disj : xs) :
∃ (f : E →L[] ), as, f a < f x
theorem geometric_hahn_banach_point_open {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {t : Set E} {x : E} (ht₁ : Convex t) (ht₂ : IsOpen t) (disj : xt) :
∃ (f : E →L[] ), bt, f x < f b
theorem geometric_hahn_banach_open_open {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {t : Set E} (hs₁ : Convex s) (hs₂ : IsOpen s) (ht₁ : Convex t) (ht₃ : IsOpen t) (disj : Disjoint s t) :
∃ (f : E →L[] ) (u : ), (as, f a < u) bt, u < f b
theorem geometric_hahn_banach_compact_closed {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {t : Set E} [LocallyConvexSpace E] (hs₁ : Convex s) (hs₂ : IsCompact s) (ht₁ : Convex t) (ht₂ : IsClosed t) (disj : Disjoint s t) :
∃ (f : E →L[] ) (u : ) (v : ), (as, f a < u) u < v bt, 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.

theorem geometric_hahn_banach_closed_compact {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {t : Set E} [LocallyConvexSpace E] (hs₁ : Convex s) (hs₂ : IsClosed s) (ht₁ : Convex t) (ht₂ : IsCompact t) (disj : Disjoint s t) :
∃ (f : E →L[] ) (u : ) (v : ), (as, f a < u) u < v bt, 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.

theorem geometric_hahn_banach_point_closed {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {t : Set E} {x : E} [LocallyConvexSpace E] (ht₁ : Convex t) (ht₂ : IsClosed t) (disj : xt) :
∃ (f : E →L[] ) (u : ), f x < u bt, u < f b
theorem geometric_hahn_banach_closed_point {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} {x : E} [LocallyConvexSpace E] (hs₁ : Convex s) (hs₂ : IsClosed s) (disj : xs) :
∃ (f : E →L[] ) (u : ), (as, f a < u) u < f x
theorem geometric_hahn_banach_point_point {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {x : E} {y : E} [LocallyConvexSpace E] [T1Space E] (hxy : x y) :
∃ (f : E →L[] ), f x < f y

See also NormedSpace.eq_iff_forall_dual_eq.

theorem iInter_halfspaces_eq {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module E] [ContinuousSMul E] {s : Set E} [LocallyConvexSpace E] (hs₁ : Convex s) (hs₂ : IsClosed s) :
⋂ (l : E →L[] ), {x : E | ∃ y ∈ s, l x l y} = s

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