[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged

src/analysis/normed/group/pointwise.lean

@@ -55,6 +55,18 @@ eq_of_forall_le_iff $ λ r, by simp_rw [le_inf_edist, ←image_inv, ball_image_i
 lemma inf_edist_inv_inv (x : E) (s : set E) : inf_edist x⁻¹ s⁻¹ = inf_edist x s :=
 by rw [inf_edist_inv, inv_inv]
 
+@[to_additive] lemma diam_mul_le (x y : set E) :
+  emetric.diam (x * y) ≤ emetric.diam x + emetric.diam y :=
+begin
+  refine emetric.diam_le _,
+  intros x' hx' y' hy',
+  simp_rw set.mem_mul at hx' hy',
+  obtain ⟨xx, xy, hxx, hxy, rfl⟩ := hx',
+  obtain ⟨yx, yy, hyx, hyy, rfl⟩ := hy',
+  exact (edist_mul_mul_le _ _ _ _).trans
+    (add_le_add (emetric.edist_le_diam_of_mem hxx hyx) (emetric.edist_le_diam_of_mem hxy hyy)),
+end
+
 end emetric
 
 variables (ε δ s t x y)

src/analysis/normed_space/basic.lean

@@ -22,7 +22,7 @@ about these definitions.
 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
 open filter metric function set
-open_locale topology big_operators nnreal ennreal uniformity pointwise
+open_locale topology big_operators nnreal ennreal uniformity
 
 section seminormed_add_comm_group
 
@@ -112,6 +112,10 @@ lemma nndist_smul₀ [normed_space α β] (s : α) (x y : β) :
   nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
 nnreal.eq $ dist_smul₀ s x y
 
+lemma edist_smul₀ [normed_space α β] (s : α) (x y : β) :
+  edist (s • x) (s • y) = ‖s‖₊ • edist x y :=
+by simp only [edist_nndist, nndist_smul₀, ennreal.coe_mul, ennreal.smul_def, smul_eq_mul]
+
 lemma lipschitz_with_smul [normed_space α β] (s : α) : lipschitz_with ‖s‖₊ ((•) s : β → β) :=
 lipschitz_with_iff_dist_le_mul.2 $ λ x y, by rw [dist_smul₀, coe_nnnorm]
 

src/analysis/normed_space/pointwise.lean

@@ -26,6 +26,35 @@ variables {𝕜 E : Type*} [normed_field 𝕜]
 section seminormed_add_comm_group
 variables [seminormed_add_comm_group E] [normed_space 𝕜 E]
 
+lemma ediam_smul₀ (c : 𝕜) (s : set E) :
+  emetric.diam (c • s) = ‖c‖₊ • emetric.diam s :=
+begin
+  obtain rfl | hc := eq_or_ne c 0,
+  { obtain rfl | hs := s.eq_empty_or_nonempty,
+    { simp },
+    simp [zero_smul_set hs, ←set.singleton_zero], },
+  refine le_antisymm _ _,
+  { simpa using (lipschitz_with_smul c).ediam_image_le s },
+  { simpa [←set.image_smul, set.image_image, inv_smul_smul₀, hc, ←ennreal.mul_le_iff_le_inv]
+      using (lipschitz_with_smul c⁻¹).ediam_image_le (c • s) }
+end
+
+lemma diam_smul₀ (c : 𝕜) (x : set E) : diam (c • x) = ‖c‖ * diam x :=
+by simp_rw [diam, ediam_smul₀, ennreal.to_real_smul, nnreal.smul_def, coe_nnnorm, smul_eq_mul]
+
+lemma inf_edist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : set E) (x : E) :
+  emetric.inf_edist (c • x) (c • s) = ‖c‖₊ • emetric.inf_edist x s :=
+begin
+  simp_rw [emetric.inf_edist],
+  have : function.surjective ((•) c : E → E) :=
+    function.right_inverse.surjective (smul_inv_smul₀ hc),
+  transitivity ⨅ y (H : y ∈ s), ‖c‖₊ • edist x y,
+  { refine (this.infi_congr _ $ λ y, _).symm,
+    simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀] },
+  { have : (‖c‖₊ : ennreal) ≠ 0 := by simp [hc],
+    simp_rw [ennreal.smul_def, smul_eq_mul, ennreal.mul_infi_of_ne this ennreal.coe_ne_top] },
+end
+
 theorem smul_ball {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
   c • ball x r = ball (c • x) (‖c‖ * r) :=
 begin

src/data/real/ennreal.lean

@@ -1243,9 +1243,17 @@ begin
   simpa [left_ne_zero_of_mul_eq_one h] using h,
 end
 
-lemma mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : (r * a ≤ b ↔ a ≤ r⁻¹ * b) :=
+lemma mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : r * a ≤ b ↔ a ≤ r⁻¹ * b :=
 by rw [←@ennreal.mul_le_mul_left _ a _ hr₀ hr₁, ←mul_assoc, ennreal.mul_inv_cancel hr₀ hr₁, one_mul]
 
+/-- A variant of `le_inv_smul_iff` that holds for `ennreal`. -/
+lemma le_inv_smul_iff {a b : ℝ≥0∞} {r : ℝ≥0} (hr₀ : r ≠ 0) : a ≤ r⁻¹ • b ↔ r • a ≤ b :=
+by simpa [hr₀, ennreal.smul_def] using (mul_le_iff_le_inv (coe_ne_zero.mpr hr₀) coe_ne_top).symm
+
+/-- A variant of `inv_smul_le_iff` that holds for `ennreal`. -/
+lemma inv_smul_le_iff {a b : ℝ≥0∞} {r : ℝ≥0} (hr₀ : r ≠ 0) : r⁻¹ • a ≤ b ↔ a ≤ r • b :=
+by simpa only [inv_inv] using (le_inv_smul_iff (inv_ne_zero hr₀)).symm
+
 lemma le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y :=
 begin
   refine le_of_forall_ge_of_dense (λ r hr, _),

src/topology/metric_space/basic.lean

@@ -52,7 +52,7 @@ metric, pseudo_metric, dist
 
 open set filter topological_space bornology
 
-open_locale uniformity topology big_operators filter nnreal ennreal
+open_locale uniformity topology big_operators filter nnreal ennreal pointwise
 
 universes u v w
 variables {α : Type u} {β : Type v} {X ι : Type*}
@@ -2389,6 +2389,8 @@ diam_subsingleton subsingleton_empty
 @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
 diam_subsingleton subsingleton_singleton
 
+@[simp, to_additive] lemma diam_one [has_one α] : diam (1 : set α) = 0 := diam_singleton
+
 -- Does not work as a simp-lemma, since {x, y} reduces to (insert y {x})
 lemma diam_pair : diam ({x, y} : set α) = dist x y :=
 by simp only [diam, emetric.diam_pair, dist_edist]

src/topology/metric_space/emetric_space.lean

@@ -32,7 +32,7 @@ to `emetric_space` at the end.
 
 open set filter classical
 
-open_locale uniformity topology big_operators filter nnreal ennreal
+open_locale uniformity topology big_operators filter nnreal ennreal pointwise
 
 universes u v w
 variables {α : Type u} {β : Type v} {X : Type*}
@@ -793,6 +793,8 @@ diam_subsingleton subsingleton_empty
 @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
 diam_subsingleton subsingleton_singleton
 
+@[simp, to_additive] lemma diam_one [has_one α] : diam (1 : set α) = 0 := diam_singleton
+
 lemma diam_Union_mem_option {ι : Type*} (o : option ι) (s : ι → set α) :
   diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) :=
 by cases o; simp

src/topology/metric_space/hausdorff_distance.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import analysis.specific_limits.basic
 import topology.metric_space.isometry
+import topology.metric_space.isometric_smul
 import topology.instances.ennreal
 
 /-!
@@ -30,7 +31,7 @@ This files introduces:
 * `cthickening δ s`, the closed thickening by radius `δ` of a set `s` in a pseudo emetric space.
 -/
 noncomputable theory
-open_locale classical nnreal ennreal topology
+open_locale classical nnreal ennreal topology pointwise
 universes u v w
 
 open classical set function topological_space filter
@@ -167,6 +168,11 @@ lemma inf_edist_image (hΦ : isometry Φ) :
   inf_edist (Φ x) (Φ '' t) = inf_edist x t :=
 by simp only [inf_edist, infi_image, hΦ.edist_eq]
 
+@[simp, to_additive] lemma inf_edist_smul {M} [has_smul M α] [has_isometric_smul M α]
+  (c : M) (x : α) (s : set α) :
+  inf_edist (c • x) (c • s) = inf_edist x s :=
+inf_edist_image (isometry_smul _ _)
+
 lemma _root_.is_open.exists_Union_is_closed {U : set α} (hU : is_open U) :
   ∃ F : ℕ → set α, (∀ n, is_closed (F n)) ∧ (∀ n, F n ⊆ U) ∧ ((⋃ n, F n) = U) ∧ monotone F :=
 begin

src/topology/metric_space/isometric_smul.lean

@@ -67,6 +67,10 @@ variables [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smu
   edist (c • x) (c • y) = edist x y :=
 isometry_smul X c x y
 
+@[simp, to_additive] lemma ediam_smul [has_smul M X] [has_isometric_smul M X] (c : M) (s : set X) :
+  emetric.diam (c • s) = emetric.diam s :=
+(isometry_smul _ _).ediam_image s
+
 @[to_additive] lemma isometry_mul_left [has_mul M] [pseudo_emetric_space M]
   [has_isometric_smul M M] (a : M) : isometry ((*) a) :=
 isometry_smul M a
@@ -223,6 +227,11 @@ lemma nndist_smul [pseudo_metric_space X] [has_smul M X] [has_isometric_smul M X
   (c : M) (x y : X) : nndist (c • x) (c • y) = nndist x y :=
 (isometry_smul X c).nndist_eq x y
 
+@[simp, to_additive]
+lemma diam_smul [pseudo_metric_space X] [has_smul M X] [has_isometric_smul M X]
+  (c : M) (s : set X) : metric.diam (c • s) = metric.diam s :=
+(isometry_smul _ _).diam_image s
+
 @[simp, to_additive]
 lemma dist_mul_left [pseudo_metric_space M] [has_mul M] [has_isometric_smul M M]
   (a b c : M) : dist (a * b) (a * c) = dist b c :=