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

• Eidelheit's theorem
• Convex ℝ s → interior (closure s) ⊆ s

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) : ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, f a < u) ∧ ∀ 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.

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) : ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b

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) : ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ 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.

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) : ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ 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.

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) : ∃ (f : StrongDual ℝ E) (u : ℝ), f x < u ∧ ∀ b ∈ t, u < f b

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) : ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, f a < u) ∧ u < f x

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) : ⋂ (l : StrongDual ℝ E), {x : E | ∃ y ∈ s, l x ≤ l y} = s

A closed convex set is the intersection of the half-spaces containing it.

noncomputable def RCLike.extendTo𝕜'ₗ {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [ContinuousConstSMul 𝕜 E] : StrongDual ℝ E →ₗ[ℝ] StrongDual 𝕜 E

Real linear extension of continuous extension of LinearMap.extendTo𝕜'

Equations

• RCLike.extendTo𝕜'ₗ = { toFun := fun (fr : StrongDual ℝ E) => let __LinearMap := (↑fr).extendTo𝕜'; { toLinearMap := __LinearMap, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RCLike.re_extendTo𝕜'ₗ {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [ContinuousConstSMul 𝕜 E] (g : StrongDual ℝ E) (x : E) : re ((extendTo𝕜'ₗ g) x) = g x

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) : ∃ (f : StrongDual 𝕜 E), re (f x₀) = 1 ∧ ∀ x ∈ s, re (f x) < 1

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u ≤ re (f b)

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u < re (f b)

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ) (v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b)

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ) (v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b)

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), re (f x) < u ∧ ∀ b ∈ t, u < re (f b)

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) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < re (f x)

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) : ⋂ (l : StrongDual 𝕜 E), {x : E | ∃ y ∈ s, re (l x) ≤ re (l y)} = s