English
If s is convex and open and disjoint from a point x, there exists f ∈ StrongDual such that f(x) < f(a) for all a ∈ s.
Русский
Пусть s выпукло и открыто и не содержит точки x. Тогда существует f ∈ StrongDual: f(x) < f(a) для всех a ∈ s.
LaTeX
$$$\exists f\in \mathrm{StrongDual}\; E,\; \forall a\in s:\; f(a) > f(x)$$$
Lean4
/-- 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 (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 :=
by
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty
· exact ⟨0, 0, by simp, fun b _hb => le_rfl⟩
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty
· exact ⟨0, 1, fun a _ha => zero_lt_one, by simp⟩
let x₀ := b₀ - a₀
let C := x₀ +ᵥ (s - t)
have : (0 : E) ∈ C := ⟨a₀ - b₀, sub_mem_sub ha₀ hb₀, by simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]⟩
have : Convex ℝ C := (hs₁.sub ht).vadd _
have : x₀ ∉ C := by
intro hx₀
rw [← add_zero x₀] at hx₀
exact disj.zero_notMem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)
obtain ⟨f, hf₁, hf₂⟩ := separate_convex_open_set ‹0 ∈ C› ‹_› (hs₂.sub_right.vadd _) ‹x₀ ∉ C›
have forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b := by
intro a ha b hb
have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
simp only [f.map_add, f.map_sub, hf₁] at this
linarith
refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => ?_⟩
· rw [← interior_Iic]
refine interior_maximal (image_subset_iff.2 fun a ha => ?_) (f.isOpenMap_of_ne_zero ?_ _ hs₂)
· exact le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (forall_mem_image.2 <| forall_le _ ha)
· rintro rfl
simp at hf₁
· exact csInf_le ⟨f a₀, forall_mem_image.2 <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)
