feat(analysis/convex/topology): improve some lemmas (#13136)

Replace some `s` with `closure s` in the LHS of `⊆` in some lemmas.

Author: urkud

src/analysis/calculus/fderiv_symmetric.lean

@@ -98,8 +98,8 @@ begin
     rw [← smul_smul],
     apply s_conv.interior.add_smul_mem this _ ht,
     rw add_assoc at hw,
-    convert s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ using 1,
-    simp only [add_assoc, smul_add] },
+    rw [add_assoc, ← smul_add],
+    exact s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ },
   -- define a function `g` on `[0,1]` (identified with `[v, v + w]`) such that `g 1 - g 0` is the
   -- quantity to be estimated. We will check that its derivative is given by an explicit
   -- expression `g'`, that we can bound. Then the desired bound for `g 1 - g 0` follows from the

src/analysis/convex/integral.lean

@@ -256,7 +256,7 @@ begin
   by_cases h0' : μ (to_measurable μ t)ᶜ = 0,
   { rw ← ae_eq_univ at h0',
     rwa [restrict_congr_set h0', restrict_univ] at ht },
-  exact hs.open_segment_subset_interior_left ht
+  exact hs.open_segment_interior_self_subset_interior ht
     (hs.set_average_mem hsc h0' (measure_ne_top _ _) (ae_restrict_of_ae hfs) hfi.integrable_on)
     (average_mem_open_segment_compl_self (measurable_set_to_measurable μ t).null_measurable_set
       h0 h0' hfi)

src/analysis/convex/strict_convex_space.lean

@@ -93,8 +93,8 @@ begin
   have hx' := hx, have hy' := hy,
   rw [← closure_closed_ball, closure_eq_interior_union_frontier,
     frontier_closed_ball (0 : E) one_ne_zero] at hx hy,
-  cases hx, { exact (convex_closed_ball _ _).combo_mem_interior_left hx hy' ha hb.le hab },
-  cases hy, { exact (convex_closed_ball _ _).combo_mem_interior_right hx' hy ha.le hb hab },
+  cases hx, { exact (convex_closed_ball _ _).combo_interior_self_mem_interior hx hy' ha hb.le hab },
+  cases hy, { exact (convex_closed_ball _ _).combo_self_interior_mem_interior hx' hy ha.le hb hab },
   rw [interior_closed_ball (0 : E) one_ne_zero, mem_ball_zero_iff],
   have hx₁ : ∥x∥ = 1, from mem_sphere_zero_iff_norm.1 hx,
   have hy₁ : ∥y∥ = 1, from mem_sphere_zero_iff_norm.1 hy,

src/analysis/convex/topology.lean

@@ -80,58 +80,119 @@ section has_continuous_const_smul
 variables [add_comm_group E] [module ℝ E] [topological_space E]
   [topological_add_group E] [has_continuous_const_smul ℝ E]
 
-lemma convex.combo_interior_self_subset_interior {s : set E} (hs : convex ℝ s) {a b : ℝ}
+/-- If `s` is a convex set, then `a • interior s + b • closure s ⊆ interior s` for all `0 < a`,
+`0 ≤ b`, `a + b = 1`. See also `convex.combo_interior_self_subset_interior` for a weaker version. -/
+lemma convex.combo_interior_closure_subset_interior {s : set E} (hs : convex ℝ s) {a b : ℝ}
   (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
-  a • interior s + b • s ⊆ interior s :=
+  a • interior s + b • closure s ⊆ interior s :=
 interior_smul₀ ha.ne' s ▸
-  calc interior (a • s) + b • s ⊆ interior (a • s + b • s) : subset_interior_add_left
+  calc interior (a • s) + b • closure s ⊆ interior (a • s) + closure (b • s) :
+    add_subset_add subset.rfl (smul_closure_subset b s)
+  ... = interior (a • s) + b • s : by rw is_open_interior.add_closure (b • s)
+  ... ⊆ interior (a • s + b • s) : subset_interior_add_left
   ... ⊆ interior s : interior_mono $ hs.set_combo_subset ha.le hb hab
 
+/-- If `s` is a convex set, then `a • interior s + b • s ⊆ interior s` for all `0 < a`, `0 ≤ b`,
+`a + b = 1`. See also `convex.combo_interior_closure_subset_interior` for a stronger version. -/
+lemma convex.combo_interior_self_subset_interior {s : set E} (hs : convex ℝ s) {a b : ℝ}
+  (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
+  a • interior s + b • s ⊆ interior s :=
+calc a • interior s + b • s ⊆ a • interior s + b • closure s :
+  add_subset_add subset.rfl $ image_subset _ subset_closure
+... ⊆ interior s : hs.combo_interior_closure_subset_interior ha hb hab
+
+/-- If `s` is a convex set, then `a • closure s + b • interior s ⊆ interior s` for all `0 ≤ a`,
+`0 < b`, `a + b = 1`. See also `convex.combo_self_interior_subset_interior` for a weaker version. -/
+lemma convex.combo_closure_interior_subset_interior {s : set E} (hs : convex ℝ s) {a b : ℝ}
+  (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
+  a • closure s + b • interior s ⊆ interior s :=
+by { rw add_comm, exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab) }
+
+/-- If `s` is a convex set, then `a • s + b • interior s ⊆ interior s` for all `0 ≤ a`, `0 < b`,
+`a + b = 1`. See also `convex.combo_closure_interior_subset_interior` for a stronger version. -/
 lemma convex.combo_self_interior_subset_interior {s : set E} (hs : convex ℝ s) {a b : ℝ}
   (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
   a • s + b • interior s ⊆ interior s :=
 by { rw add_comm, exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab) }
 
-lemma convex.combo_mem_interior_left {s : set E} (hs : convex ℝ s) {x y : E} (hx : x ∈ interior s)
-  (hy : y ∈ s) {a b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
+lemma convex.combo_interior_closure_mem_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ interior s) (hy : y ∈ closure s) {a b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
   a • x + b • y ∈ interior s :=
-hs.combo_interior_self_subset_interior ha hb hab $
+hs.combo_interior_closure_subset_interior ha hb hab $
   add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
 
-lemma convex.combo_mem_interior_right {s : set E} (hs : convex ℝ s) {x y : E} (hx : x ∈ s)
-  (hy : y ∈ interior s) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
+lemma convex.combo_interior_self_mem_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ interior s) (hy : y ∈ s) {a b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
   a • x + b • y ∈ interior s :=
-hs.combo_self_interior_subset_interior ha hb hab $
+hs.combo_interior_closure_mem_interior hx (subset_closure hy) ha hb hab
+
+lemma convex.combo_closure_interior_mem_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ closure s) (hy : y ∈ interior s) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
+  a • x + b • y ∈ interior s :=
+hs.combo_closure_interior_subset_interior ha hb hab $
   add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
 
-lemma convex.open_segment_subset_interior_left {s : set E} (hs : convex ℝ s) {x y : E}
+lemma convex.combo_self_interior_mem_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ s) (hy : y ∈ interior s) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
+  a • x + b • y ∈ interior s :=
+hs.combo_closure_interior_mem_interior (subset_closure hx) hy ha hb hab
+
+lemma convex.open_segment_interior_closure_subset_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ interior s) (hy : y ∈ closure s) : open_segment ℝ x y ⊆ interior s :=
+begin
+  rintro _ ⟨a, b, ha, hb, hab, rfl⟩,
+  exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab
+end
+
+lemma convex.open_segment_interior_self_subset_interior {s : set E} (hs : convex ℝ s) {x y : E}
   (hx : x ∈ interior s) (hy : y ∈ s) : open_segment ℝ x y ⊆ interior s :=
-by { rintro _ ⟨a, b, ha, hb, hab, rfl⟩, exact hs.combo_mem_interior_left hx hy ha hb.le hab }
+hs.open_segment_interior_closure_subset_interior hx (subset_closure hy)
 
-lemma convex.open_segment_subset_interior_right {s : set E} (hs : convex ℝ s) {x y : E}
+lemma convex.open_segment_closure_interior_subset_interior {s : set E} (hs : convex ℝ s) {x y : E}
+  (hx : x ∈ closure s) (hy : y ∈ interior s) : open_segment ℝ x y ⊆ interior s :=
+begin
+  rintro _ ⟨a, b, ha, hb, hab, rfl⟩,
+  exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab
+end
+
+lemma convex.open_segment_self_interior_subset_interior {s : set E} (hs : convex ℝ s) {x y : E}
   (hx : x ∈ s) (hy : y ∈ interior s) : open_segment ℝ x y ⊆ interior s :=
-by { rintro _ ⟨a, b, ha, hb, hab, rfl⟩, exact hs.combo_mem_interior_right hx hy ha.le hb hab }
+hs.open_segment_closure_interior_subset_interior (subset_closure hx) hy
+
+/-- If `x ∈ closure s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`.
+-/
+lemma convex.add_smul_sub_mem_interior' {s : set E} (hs : convex ℝ s)
+  {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {t : ℝ} (ht : t ∈ Ioc (0 : ℝ) 1) :
+  x + t • (y - x) ∈ interior s :=
+by simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm]
+  using hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2)
+    (add_sub_cancel'_right _ _)
 
 /-- If `x ∈ s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`. -/
 lemma convex.add_smul_sub_mem_interior {s : set E} (hs : convex ℝ s)
   {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {t : ℝ} (ht : t ∈ Ioc (0 : ℝ) 1) :
   x + t • (y - x) ∈ interior s :=
-by simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm]
-  using hs.combo_mem_interior_left hy hx ht.1 (sub_nonneg.mpr ht.2) (add_sub_cancel'_right _ _)
+hs.add_smul_sub_mem_interior' (subset_closure hx) hy ht
+
+/-- If `x ∈ closure s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`. -/
+lemma convex.add_smul_mem_interior' {s : set E} (hs : convex ℝ s)
+  {x y : E} (hx : x ∈ closure s) (hy : x + y ∈ interior s) {t : ℝ} (ht : t ∈ Ioc (0 : ℝ) 1) :
+  x + t • y ∈ interior s :=
+by simpa only [add_sub_cancel'] using hs.add_smul_sub_mem_interior' hx hy ht
 
 /-- If `x ∈ s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`. -/
 lemma convex.add_smul_mem_interior {s : set E} (hs : convex ℝ s)
   {x y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : ℝ} (ht : t ∈ Ioc (0 : ℝ) 1) :
   x + t • y ∈ interior s :=
-by { convert hs.add_smul_sub_mem_interior hx hy ht, abel }
+hs.add_smul_mem_interior' (subset_closure hx) hy ht
 
 /-- In a topological vector space, the interior of a convex set is convex. -/
-lemma convex.interior {s : set E} (hs : convex ℝ s) : convex ℝ (interior s) :=
+protected lemma convex.interior {s : set E} (hs : convex ℝ s) : convex ℝ (interior s) :=
 convex_iff_open_segment_subset.mpr $ λ x y hx hy,
-  hs.open_segment_subset_interior_left hx (interior_subset hy)
+  hs.open_segment_closure_interior_subset_interior (interior_subset_closure hx) hy
 
 /-- In a topological vector space, the closure of a convex set is convex. -/
-lemma convex.closure {s : set E} (hs : convex ℝ s) : convex ℝ (closure s) :=
+protected lemma convex.closure {s : set E} (hs : convex ℝ s) : convex ℝ (closure s) :=
 λ x y hx hy a b ha hb hab,
 let f : E → E → E := λ x' y', a • x' + b • y' in
 have hf : continuous (λ p : E × E, f p.1 p.2), from
@@ -165,17 +226,17 @@ hs.compact_convex_hull.is_closed
 open affine_map
 
 /-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
-the result contains the original set.
+the result contains the closure of the original set.
 
 TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`. -/
-lemma convex.subset_interior_image_homothety_of_one_lt
-  {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
-  s ⊆ interior (image (homothety x t) s) :=
+lemma convex.closure_subset_interior_image_homothety_of_one_lt {s : set E} (hs : convex ℝ s)
+  {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
+  closure s ⊆ interior (homothety x t '' s) :=
 begin
   intros y hy,
   let I := { z | ∃ (u : ℝ), u ∈ Ioc (0 : ℝ) 1 ∧ z = y + u • (x - y) },
   have hI : I ⊆ interior s,
-  { rintros z ⟨u, hu, rfl⟩, exact hs.add_smul_sub_mem_interior hy hx hu, },
+  { rintros z ⟨u, hu, rfl⟩, exact hs.add_smul_sub_mem_interior' hy hx hu, },
   let z := homothety x t⁻¹ y,
   have hz₁ : z ∈ interior s,
   { suffices : z ∈ I, { exact hI this, },
@@ -190,13 +251,22 @@ begin
   rw hz₂,
   rw mem_interior at hz₁ ⊢,
   obtain ⟨U, hU₁, hU₂, hU₃⟩ := hz₁,
-  exact ⟨image (homothety x t) U,
+  exact ⟨homothety x t '' U,
          image_subset ⇑(homothety x t) hU₁,
          homothety_is_open_map x t ht' U hU₂,
          mem_image_of_mem ⇑(homothety x t) hU₃⟩,
 end
 
-lemma convex.is_path_connected {s : set E} (hconv : convex ℝ s) (hne : s.nonempty) :
+/-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
+the result contains the closure of the original set.
+
+TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`. -/
+lemma convex.subset_interior_image_homothety_of_one_lt {s : set E} (hs : convex ℝ s)
+  {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
+  s ⊆ interior (homothety x t '' s) :=
+subset_closure.trans $ hs.closure_subset_interior_image_homothety_of_one_lt hx t ht
+
+protected lemma convex.is_path_connected {s : set E} (hconv : convex ℝ s) (hne : s.nonempty) :
   is_path_connected s :=
 begin
   refine is_path_connected_iff.mpr ⟨hne, _⟩,
@@ -212,7 +282,7 @@ Every topological vector space over ℝ is path connected.
 
 Not an instance, because it creates enormous TC subproblems (turn on `pp.all`).
 -/
-lemma topological_add_group.path_connected : path_connected_space E :=
+protected lemma topological_add_group.path_connected : path_connected_space E :=
 path_connected_space_iff_univ.mpr $ convex_univ.is_path_connected ⟨(0 : E), trivial⟩
 
 end has_continuous_smul