feat(analysis/normed_space/hahn_banach/separation): generalize to (lo…

…cally convex) topological vector spaces (#16796)




Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Moritz Doll <doll@uni-bremen.de>
Co-authored-by: mcdoll <moritz.doll@googlemail.com>

src/analysis/convex/exposed.lean

@@ -45,8 +45,8 @@ More not-yet-PRed stuff is available on the branch `sperner_again`.
 open_locale classical affine big_operators
 open set
 
-variables (𝕜 : Type*) {E : Type*} [normed_linear_ordered_field 𝕜] [normed_add_comm_group E]
-  [normed_space 𝕜 E] {l : E →L[𝕜] 𝕜} {A B C : set E} {X : finset E} {x : E}
+variables (𝕜 : Type*) {E : Type*} [normed_linear_ordered_field 𝕜] [add_comm_monoid E] [module 𝕜 E]
+  [topological_space E] {l : E →L[𝕜] 𝕜} {A B C : set E} {X : finset E} {x : E}
 
 /-- A set `B` is exposed with respect to `A` iff it maximizes some functional over `A` (and contains
 all points maximizing it). Written `is_exposed 𝕜 A B`. -/
@@ -197,8 +197,8 @@ begin
   exact hA.is_closed_le continuous_on_const l.continuous.continuous_on,
 end
 
-protected lemma is_compact [order_closed_topology 𝕜] (hAB : is_exposed 𝕜 A B) (hA : is_compact A) :
-  is_compact B :=
+protected lemma is_compact [order_closed_topology 𝕜] [t2_space E] (hAB : is_exposed 𝕜 A B)
+  (hA : is_compact A) : is_compact B :=
 compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset
 
 end is_exposed

src/analysis/convex/gauge.lean

@@ -113,10 +113,15 @@ lemma gauge_nonneg (x : E) : 0 ≤ gauge s x := real.Inf_nonneg _ $ λ x hx, hx.
 lemma gauge_neg (symmetric : ∀ x ∈ s, -x ∈ s) (x : E) : gauge s (-x) = gauge s x :=
 begin
   have : ∀ x, -x ∈ s ↔ x ∈ s := λ x, ⟨λ h, by simpa using symmetric _ h, symmetric x⟩,
-  rw [gauge_def', gauge_def'],
-  simp_rw [smul_neg, this],
+  simp_rw [gauge_def', smul_neg, this]
 end
 
+lemma gauge_neg_set_neg (x : E) : gauge (-s) (-x) = gauge s x :=
+by simp_rw [gauge_def', smul_neg, neg_mem_neg]
+
+lemma gauge_neg_set_eq_gauge_neg (x : E) : gauge (-s) x = gauge s (-x) :=
+by rw [← gauge_neg_set_neg, neg_neg]
+
 lemma gauge_le_of_mem (ha : 0 ≤ a) (hx : x ∈ a • s) : gauge s x ≤ a :=
 begin
   obtain rfl | ha' := ha.eq_or_lt,

src/analysis/convex/krein_milman.lean

@@ -47,19 +47,15 @@ matrices, permutation matrices being the extreme points.
 
 See chapter 8 of [Barry Simon, *Convexity*][simon2011]
 
-## TODO
-
-* Both theorems are currently stated for normed `ℝ`-spaces due to our version of geometric
-  Hahn-Banach. They are more generally true in a LCTVS without changes to the proofs.
 -/
 
 open set
 open_locale classical
 
-variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] {s : set E}
+variables {E : Type*} [add_comm_group E] [module ℝ E] [topological_space E] [t2_space E]
+  [topological_add_group E] [has_continuous_smul ℝ E] [locally_convex_space ℝ E] {s : set E}
 
-/-- **Krein-Milman lemma**: In a LCTVS (currently only in normed `ℝ`-spaces), any nonempty compact
-set has an extreme point. -/
+/-- **Krein-Milman lemma**: In a LCTVS, any nonempty compact set has an extreme point. -/
 lemma is_compact.has_extreme_point (hscomp : is_compact s) (hsnemp : s.nonempty) :
   (s.extreme_points ℝ).nonempty :=
 begin
@@ -89,8 +85,8 @@ begin
   exacts [⟨t, subset.rfl, htu⟩, ⟨u, hut, subset.rfl⟩],
 end
 
-/-- **Krein-Milman theorem**: In a LCTVS (currently only in normed `ℝ`-spaces), any compact convex
-set is the closure of the convex hull of its extreme points. -/
+/-- **Krein-Milman theorem**: In a LCTVS, any compact convex set is the closure of the convex hull
+    of its extreme points. -/
 lemma closure_convex_hull_extreme_points (hscomp : is_compact s) (hAconv : convex ℝ s) :
   closure (convex_hull ℝ $ s.extreme_points ℝ) = s :=
 begin

src/analysis/normed_space/hahn_banach/separation.lean

@@ -39,29 +39,28 @@ variables {𝕜 E : Type*}
 /-- 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`. -/
-lemma separate_convex_open_set [seminormed_add_comm_group E] [normed_space ℝ E] {s : set E}
+lemma separate_convex_open_set [topological_space E] [add_comm_group E] [topological_add_group E]
+  [module ℝ E] [has_continuous_smul ℝ E] {s : set E}
   (hs₀ : (0 : E) ∈ s) (hs₁ : convex ℝ s) (hs₂ : is_open s) {x₀ : E} (hx₀ : x₀ ∉ s) :
   ∃ f : E →L[ℝ] ℝ, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1 :=
 begin
   let f : E →ₗ.[ℝ] ℝ :=
     linear_pmap.mk_span_singleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm,
-  obtain ⟨r, hr, hrs⟩ := metric.mem_nhds_iff.1
-    (filter.inter_mem (hs₂.mem_nhds hs₀) $ hs₂.neg.mem_nhds $ by rwa [mem_neg, neg_zero]),
   obtain ⟨φ, hφ₁, hφ₂⟩ := exists_extension_of_le_sublinear f (gauge s)
     (λ c hc, gauge_smul_of_nonneg hc.le)
     (gauge_add_le hs₁ $ absorbent_nhds_zero $ hs₂.mem_nhds hs₀) _,
-  { refine ⟨φ.mk_continuous (r⁻¹) $ λ x, _, _, _⟩,
-    { rw [real.norm_eq_abs, abs_le, neg_le, ←linear_map.map_neg],
-      nth_rewrite 0 ←norm_neg x,
-      suffices : ∀ x, φ x ≤ r⁻¹ * ∥x∥,
-      { exact ⟨this _, this _⟩ },
-      refine λ x, (hφ₂ _).trans _,
-      rw [←div_eq_inv_mul, ←gauge_ball hr],
-      exact gauge_mono (absorbent_ball_zero hr) (hrs.trans $ inter_subset_left _ _) x },
-    { dsimp,
-      rw [←submodule.coe_mk x₀ (submodule.mem_span_singleton_self _), hφ₁,
-        linear_pmap.mk_span_singleton'_apply_self] },
-    { exact λ x hx, (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_open hs₁ hs₀ hs₂ hx) } },
+  have hφ₃ : φ x₀ = 1,
+  { rw [←submodule.coe_mk x₀ (submodule.mem_span_singleton_self _), hφ₁,
+      linear_pmap.mk_span_singleton'_apply_self] },
+  have hφ₄ : ∀ x ∈ s, φ x < 1,
+  { exact λ x hx, (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_open hs₁ hs₀ hs₂ hx) },
+  { refine ⟨⟨φ, _⟩, hφ₃, hφ₄⟩,
+    refine φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (nonempty.vadd_set ⟨0, hs₀⟩)
+      (vadd_set_subset_iff.mpr $ λ x hx, _),
+    change φ (-x₀ + x) ≠ 0,
+    rw [map_add, map_neg],
+    specialize hφ₄ x hx,
+    linarith },
   rintro ⟨x, hx⟩,
   obtain ⟨y, rfl⟩ := submodule.mem_span_singleton.1 hx,
   rw linear_pmap.mk_span_singleton'_apply,
@@ -70,11 +69,12 @@ begin
   { exact h.trans (gauge_nonneg _) },
   { rw [gauge_smul_of_nonneg h.le, smul_eq_mul, le_mul_iff_one_le_right h],
     exact one_le_gauge_of_not_mem (hs₁.star_convex hs₀)
-      ((absorbent_ball_zero hr).subset $ hrs.trans $ inter_subset_left _ _).absorbs hx₀,
+      (absorbent_nhds_zero $ hs₂.mem_nhds hs₀).absorbs hx₀,
     apply_instance }
 end
 
-variables [normed_add_comm_group E] [normed_space ℝ E] {s t : set E} {x y : E}
+variables [topological_space E] [add_comm_group E] [topological_add_group E] [module ℝ E]
+  [has_continuous_smul ℝ E] {s t : set E} {x y : E}
 
 /-- 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. -/
@@ -141,6 +141,8 @@ begin
   exact (hf₁ _ ha₀).not_le (hf₂ _ hb₀),
 end
 
+variables [locally_convex_space ℝ E]
+
 /-- 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_compact_closed (hs₁ : convex ℝ s) (hs₂ : is_compact s)
@@ -179,8 +181,9 @@ let ⟨f, s, t, ha, hst, hb⟩ := geometric_hahn_banach_closed_compact hs₁ hs
   is_compact_singleton (disjoint_singleton_right.2 disj)
   in ⟨f, s, ha, hst.trans $ hb x $ mem_singleton _⟩
 
-/-- Special case of `normed_space.eq_iff_forall_dual_eq`. -/
-theorem geometric_hahn_banach_point_point (hxy : x ≠ y) : ∃ (f : E →L[ℝ] ℝ), f x < f y :=
+/-- See also `normed_space.eq_iff_forall_dual_eq`. -/
+theorem geometric_hahn_banach_point_point [t1_space E] (hxy : x ≠ y) :
+  ∃ (f : E →L[ℝ] ℝ), f x < f y :=
 begin
   obtain ⟨f, s, t, hs, st, ht⟩ :=
     geometric_hahn_banach_compact_closed (convex_singleton x) is_compact_singleton

src/topology/algebra/const_mul_action.lean

@@ -206,6 +206,9 @@ is_closed_map_smul c s hs
 @[to_additive] lemma closure_smul (c : G) (s : set α) : closure (c • s) = c • closure s :=
 ((homeomorph.smul c).image_closure s).symm
 
+@[to_additive] lemma dense.smul (c : G) {s : set α} (hs : dense s) : dense (c • s) :=
+by rw [dense_iff_closure_eq] at ⊢ hs; rw [closure_smul, hs, smul_set_univ]
+
 @[to_additive] lemma interior_smul (c : G) (s : set α) : interior (c • s) = c • interior s :=
 ((homeomorph.smul c).image_interior s).symm