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 ∧ βˆ€ 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 : Set E} {t : Set E} [TopologicalAddGroup E] [ContinuousSMul ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (ht : Convex ℝ t) (disj : Disjoint s t) :
βˆƒ (f : E β†’L[ℝ] ℝ) (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} [TopologicalAddGroup E] [ContinuousSMul ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (disj : x βˆ‰ s) :
βˆƒ (f : E β†’L[ℝ] ℝ), βˆ€ 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} [TopologicalAddGroup E] [ContinuousSMul ℝ E] (ht₁ : Convex ℝ t) (htβ‚‚ : IsOpen t) (disj : x βˆ‰ t) :
βˆƒ (f : E β†’L[ℝ] ℝ), βˆ€ b ∈ t, f x < f b
theorem geometric_hahn_banach_open_open {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Set E} [TopologicalAddGroup E] [ContinuousSMul ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (ht₁ : Convex ℝ t) (ht₃ : IsOpen t) (disj : Disjoint s t) :
βˆƒ (f : E β†’L[ℝ] ℝ) (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 : Set E} {t : Set E} [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsCompact s) (ht₁ : Convex ℝ t) (htβ‚‚ : IsClosed t) (disj : Disjoint s t) :
βˆƒ (f : E β†’L[ℝ] ℝ) (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 : Set E} {t : Set E} [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsClosed s) (ht₁ : Convex ℝ t) (htβ‚‚ : IsCompact t) (disj : Disjoint s t) :
βˆƒ (f : E β†’L[ℝ] ℝ) (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} [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (ht₁ : Convex ℝ t) (htβ‚‚ : IsClosed t) (disj : x βˆ‰ t) :
βˆƒ (f : E β†’L[ℝ] ℝ) (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} [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsClosed s) (disj : x βˆ‰ s) :
βˆƒ (f : E β†’L[ℝ] ℝ) (u : ℝ), (βˆ€ a ∈ s, f a < u) ∧ u < f x

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} [TopologicalAddGroup E] [ContinuousSMul ℝ 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.

noncomputable def RCLike.extendToπ•œ'β‚— {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [ContinuousConstSMul π•œ E] :

Real linear extension of continuous extension of LinearMap.extendToπ•œ'

Equations
  • RCLike.extendToπ•œ'β‚— = { toFun := fun (fr : E β†’L[ℝ] ℝ) => { toLinearMap := (↑fr).extendToπ•œ', cont := β‹― }, map_add' := β‹―, map_smul' := β‹― }
Instances For
    @[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 : E β†’L[ℝ] ℝ) (x : E) :
    RCLike.re ((RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {s : Set E} (hsβ‚€ : 0 ∈ s) (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) {xβ‚€ : E} (hxβ‚€ : xβ‚€ βˆ‰ s) :
    βˆƒ (f : E β†’L[π•œ] π•œ), RCLike.re (f xβ‚€) = 1 ∧ βˆ€ x ∈ s, RCLike.re (f x) < 1
    theorem RCLike.geometric_hahn_banach_open {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Set E} [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (ht : Convex ℝ t) (disj : Disjoint s t) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ), (βˆ€ a ∈ s, RCLike.re (f a) < u) ∧ βˆ€ b ∈ t, u ≀ RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (disj : x βˆ‰ s) :
    βˆƒ (f : E β†’L[π•œ] π•œ), βˆ€ a ∈ s, RCLike.re (f a) < RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (ht₁ : Convex ℝ t) (htβ‚‚ : IsOpen t) (disj : x βˆ‰ t) :
    βˆƒ (f : E β†’L[π•œ] π•œ), βˆ€ b ∈ t, RCLike.re (f x) < RCLike.re (f b)
    theorem RCLike.geometric_hahn_banach_open_open {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Set E} [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsOpen s) (ht₁ : Convex ℝ t) (ht₃ : IsOpen t) (disj : Disjoint s t) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ), (βˆ€ a ∈ s, RCLike.re (f a) < u) ∧ βˆ€ b ∈ t, u < RCLike.re (f b)
    theorem RCLike.geometric_hahn_banach_compact_closed {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Set E} [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsCompact s) (ht₁ : Convex ℝ t) (htβ‚‚ : IsClosed t) (disj : Disjoint s t) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ) (v : ℝ), (βˆ€ a ∈ s, RCLike.re (f a) < u) ∧ u < v ∧ βˆ€ b ∈ t, v < RCLike.re (f b)
    theorem RCLike.geometric_hahn_banach_closed_compact {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {s : Set E} {t : Set E} [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsClosed s) (ht₁ : Convex ℝ t) (htβ‚‚ : IsCompact t) (disj : Disjoint s t) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ) (v : ℝ), (βˆ€ a ∈ s, RCLike.re (f a) < u) ∧ u < v ∧ βˆ€ b ∈ t, v < RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] (ht₁ : Convex ℝ t) (htβ‚‚ : IsClosed t) (disj : x βˆ‰ t) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ), RCLike.re (f x) < u ∧ βˆ€ b ∈ t, u < RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsClosed s) (disj : x βˆ‰ s) :
    βˆƒ (f : E β†’L[π•œ] π•œ) (u : ℝ), (βˆ€ a ∈ s, RCLike.re (f a) < u) ∧ u < RCLike.re (f x)
    theorem RCLike.geometric_hahn_banach_point_point {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] {x : E} {y : E} [RCLike π•œ] [Module π•œ E] [IsScalarTower ℝ π•œ E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] [T1Space E] (hxy : x β‰  y) :
    βˆƒ (f : E β†’L[π•œ] π•œ), RCLike.re (f x) < RCLike.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] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [LocallyConvexSpace ℝ E] (hs₁ : Convex ℝ s) (hsβ‚‚ : IsClosed s) :
    β‹‚ (l : E β†’L[π•œ] π•œ), {x : E | βˆƒ y ∈ s, RCLike.re (l x) ≀ RCLike.re (l y)} = s