feat(analysis/convex/topology): add lemmas (#11615)

Author: urkud

src/analysis/convex/topology.lean

@@ -79,21 +79,55 @@ section has_continuous_smul
 variables [add_comm_group E] [module ℝ E] [topological_space E]
   [topological_add_group E] [has_continuous_smul ℝ E]
 
+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 :=
+interior_smul₀ ha.ne' s ▸
+  calc interior (a • s) + b • s ⊆ interior (a • s + b • s) : subset_interior_add_left
+  ... ⊆ interior s : interior_mono $ hs.set_combo_subset ha.le hb hab
+
+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) :
+  a • x + b • y ∈ interior s :=
+hs.combo_interior_self_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) :
+  a • x + b • y ∈ interior s :=
+hs.combo_self_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}
+  (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 }
+
+lemma convex.open_segment_subset_interior_right {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 }
+
+/-- 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 _ _)
+
+/-- 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 }
+
 /-- 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) :=
-convex_iff_pointwise_add_subset.mpr $ λ a b ha hb hab,
-  have h : is_open (a • interior s + b • interior s), from
-  or.elim (classical.em (a = 0))
-  (λ heq,
-    have hne : b ≠ 0, by { rw [heq, zero_add] at hab, rw hab, exact one_ne_zero },
-    by { rw ← image_smul,
-         exact (is_open_map_smul₀ hne _ is_open_interior).add_left } )
-  (λ hne,
-    by { rw ← image_smul,
-         exact (is_open_map_smul₀ hne _ is_open_interior).add_right }),
-  (subset_interior_iff_subset_of_open h).mpr $ subset.trans
-    (by { simp only [← image_smul], apply add_subset_add; exact image_subset _ interior_subset })
-    (convex_iff_pointwise_add_subset.mp hs ha hb hab)
+convex_iff_open_segment_subset.mpr $ λ x y hx hy,
+  hs.open_segment_subset_interior_left hx (interior_subset 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) :=
@@ -120,25 +154,6 @@ lemma set.finite.is_closed_convex_hull [t2_space E] {s : set E} (hs : finite s)
   is_closed (convex_hull ℝ s) :=
 hs.compact_convex_hull.is_closed
 
-/-- 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 :=
-begin
-  let f := λ z, x + t • (z - x),
-  have : is_open_map f := (is_open_map_add_left _).comp
-    ((is_open_map_smul (units.mk0 _ ht.1.ne')).comp (is_open_map_sub_right _)),
-  apply mem_interior.2 ⟨f '' (interior s), _, this _ is_open_interior, mem_image_of_mem _ hy⟩,
-  refine image_subset_iff.2 (λ z hz, _),
-  exact hs.add_smul_sub_mem hx (interior_subset hz) ⟨ht.1.le, ht.2⟩,
-end
-
-/-- 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 }
-
 open affine_map
 
 /-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of

src/topology/algebra/group.lean

@@ -130,7 +130,7 @@ section pointwise
 variables [topological_space α] [group α] [has_continuous_mul α] {s t : set α}
 
 @[to_additive]
-lemma is_open.mul_left (ht : is_open t) :  is_open (s * t) :=
+lemma is_open.mul_left (ht : is_open t) : is_open (s * t) :=
 begin
   rw ←Union_mul_left_image,
   exact is_open_Union (λ a, is_open_Union $ λ ha, is_open_map_mul_left a t ht),

src/topology/algebra/ordered/basic.lean

@@ -209,6 +209,16 @@ lemma is_closed.is_closed_le [topological_space β] {f g : β → α} {s : set 
   is_closed {x ∈ s | f x ≤ g x} :=
 (hf.prod hg).preimage_closed_of_closed hs order_closed_topology.is_closed_le'
 
+lemma is_closed.epigraph [topological_space β] {f : β → α} {s : set β}
+  (hs : is_closed s) (hf : continuous_on f s) :
+  is_closed {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
+(hs.preimage continuous_fst).is_closed_le (hf.comp continuous_on_fst subset.rfl) continuous_on_snd
+
+lemma is_closed.hypograph [topological_space β] {f : β → α} {s : set β}
+  (hs : is_closed s) (hf : continuous_on f s) :
+  is_closed {p : β × α | p.1 ∈ s ∧ p.2 ≤ f p.1} :=
+(hs.preimage continuous_fst).is_closed_le continuous_on_snd (hf.comp continuous_on_fst subset.rfl)
+
 omit t
 
 lemma nhds_within_Ici_ne_bot {a b : α} (H₂ : a ≤ b) :