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:
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_of_nonempty_interior': One set has nonempty interior. Nonstrict separation.geometric_hahn_banach_of_nonempty_interior: One set has nonempty interior, the other one is nonempty. Nonstrict separation by a nonzero functional.geometric_hahn_banach_of_nonempty_interior_point: One set has nonempty interior, the other one is a singleton outside this interior. Nonstrict separation, with the maximum attained at the singleton.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.
theorem
separate_convex_open_set
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[IsTopologicalAddGroup E]
[Module ℝ E]
[ContinuousSMul ℝ E]
{s : Set E}
(hs₀ : 0 ∈ s)
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
{x₀ : E}
(hx₀ : x₀ ∉ s)
:
∃ (f : StrongDual ℝ E), f x₀ = 1 ∧ ∀ 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.
theorem
geometric_hahn_banach_open
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(ht : Convex ℝ t)
(disj : Disjoint s t)
:
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]
[Module ℝ E]
{s : Set E}
{x : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(disj : x ∉ s)
:
∃ (f : StrongDual ℝ E), ∀ a ∈ s, f a < f x
theorem
geometric_hahn_banach_point_open
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{t : Set E}
{x : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(ht₁ : Convex ℝ t)
(ht₂ : IsOpen t)
(disj : x ∉ t)
:
∃ (f : StrongDual ℝ E), ∀ b ∈ t, f x < f b
theorem
geometric_hahn_banach_open_open
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(ht₁ : Convex ℝ t)
(ht₃ : IsOpen t)
(disj : Disjoint s t)
:
theorem
geometric_hahn_banach_of_nonempty_interior
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(hs : Convex ℝ s)
(ht : Convex ℝ t)
(hst : Disjoint (interior s) t)
(hsint : (interior s).Nonempty)
(htne : t.Nonempty)
:
If s and t are convex, interior s is nonempty and disjoint from t, then a nonzero
continuous linear functional weakly separates s and t. The proof first separates interior s
from t, then extends the inequality from interior s to all of s using
closure (interior s) = closure s.
theorem
geometric_hahn_banach_of_nonempty_interior'
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
(hs : Convex ℝ s)
(ht : Convex ℝ t)
(hst : Disjoint (interior s) t)
(hsint : (interior s).Nonempty)
:
If s and t are convex, interior s is nonempty and disjoint from t, then a continuous
linear functional weakly separates s and t. If t is nonempty, this follows from
geometric_hahn_banach_of_nonempty_interior; if t = ∅, the zero functional works.
theorem
geometric_hahn_banach_of_nonempty_interior_point
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{x : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
{A : Set E}
(hA : Convex ℝ A)
(hxA : x ∉ interior A)
(hAint : (interior A).Nonempty)
:
∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, f a ≤ f x
If A is convex with nonempty interior and x ∉ interior A, then there is a nonzero
continuous linear functional whose maximum on A is attained at x.
theorem
geometric_hahn_banach_compact_closed
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsCompact s)
(ht₁ : Convex ℝ t)
(ht₂ : IsClosed t)
(disj : Disjoint s t)
:
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]
[Module ℝ E]
{s t : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
(ht₁ : Convex ℝ t)
(ht₂ : IsCompact t)
(disj : Disjoint s t)
:
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]
[Module ℝ E]
{t : Set E}
{x : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
(ht₁ : Convex ℝ t)
(ht₂ : IsClosed t)
(disj : x ∉ t)
:
theorem
geometric_hahn_banach_closed_point
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
{x : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
(disj : x ∉ s)
:
theorem
geometric_hahn_banach_point_point
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{x y : E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
[T1Space E]
(hxy : x ≠ y)
:
∃ (f : StrongDual ℝ E), f x < f y
See also NormedSpace.eq_iff_forall_dual_eq.
theorem
iInter_halfSpaces_eq
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
:
A closed convex set is the intersection of the half-spaces containing it.
theorem
RCLike.separate_convex_open_set
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
{s : Set E}
(hs₀ : 0 ∈ s)
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
{x₀ : E}
(hx₀ : x₀ ∉ s)
:
theorem
RCLike.geometric_hahn_banach_open
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(ht : Convex ℝ t)
(disj : Disjoint s t)
:
theorem
RCLike.geometric_hahn_banach_open_point
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
{x : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(disj : x ∉ s)
:
∃ (f : StrongDual 𝕜 E), ∀ a ∈ s, re (f a) < re (f x)
theorem
RCLike.geometric_hahn_banach_point_open
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{t : Set E}
{x : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(ht₁ : Convex ℝ t)
(ht₂ : IsOpen t)
(disj : x ∉ t)
:
∃ (f : StrongDual 𝕜 E), ∀ b ∈ t, re (f x) < re (f b)
theorem
RCLike.geometric_hahn_banach_open_open
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(hs₁ : Convex ℝ s)
(hs₂ : IsOpen s)
(ht₁ : Convex ℝ t)
(ht₃ : IsOpen t)
(disj : Disjoint s t)
:
theorem
RCLike.geometric_hahn_banach_of_nonempty_interior
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(hs : Convex ℝ s)
(ht : Convex ℝ t)
(hst : Disjoint (interior s) t)
(hsint : (interior s).Nonempty)
(htne : t.Nonempty)
:
theorem
RCLike.geometric_hahn_banach_of_nonempty_interior'
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(hs : Convex ℝ s)
(ht : Convex ℝ t)
(hst : Disjoint (interior s) t)
(hsint : (interior s).Nonempty)
:
If s and t are convex, interior s is nonempty and disjoint from t, then a continuous
𝕜-linear functional weakly separates s and t. If t is nonempty, this follows from
geometric_hahn_banach_of_nonempty_interior; if t = ∅, the zero functional works.
theorem
RCLike.geometric_hahn_banach_of_nonempty_interior_point
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{x : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
{A : Set E}
(hA : Convex ℝ A)
(hxA : x ∉ interior A)
(hAint : (interior A).Nonempty)
:
If A is convex with nonempty interior and x ∉ interior A, then there is a nonzero
continuous 𝕜-linear functional whose real part attains its maximum on A at x.
theorem
RCLike.geometric_hahn_banach_compact_closed
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsCompact s)
(ht₁ : Convex ℝ t)
(ht₂ : IsClosed t)
(disj : Disjoint s t)
:
theorem
RCLike.geometric_hahn_banach_closed_compact
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s t : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
(ht₁ : Convex ℝ t)
(ht₂ : IsCompact t)
(disj : Disjoint s t)
:
theorem
RCLike.geometric_hahn_banach_point_closed
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{t : Set E}
{x : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(ht₁ : Convex ℝ t)
(ht₂ : IsClosed t)
(disj : x ∉ t)
:
theorem
RCLike.geometric_hahn_banach_closed_point
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
{x : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
(disj : x ∉ s)
:
theorem
RCLike.geometric_hahn_banach_point_point
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{x y : E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
[T1Space E]
(hxy : x ≠ y)
:
∃ (f : StrongDual 𝕜 E), re (f x) < re (f y)
theorem
RCLike.iInter_halfSpaces_eq
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
:
theorem
RCLike.iInter_halfSpaces_eq'
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
:
theorem
RCLike.iInter_countable_halfSpaces_eq
{𝕜 : Type u_1}
{E : Type u_2}
[TopologicalSpace E]
[AddCommGroup E]
[Module ℝ E]
{s : Set E}
[RCLike 𝕜]
[Module 𝕜 E]
[IsScalarTower ℝ 𝕜 E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyConvexSpace ℝ E]
[HereditarilyLindelofSpace E]
(hs₁ : Convex ℝ s)
(hs₂ : IsClosed s)
: