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_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 #
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_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_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)
: