feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged (#18990)

Author: eric-wieser

src/analysis/normed/mul_action.lean

@@ -34,7 +34,10 @@ by simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y
 lemma nndist_smul_le (s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y :=
 dist_smul_le s x y
 
-lemma lipschitz_with_smul  (s : α) : lipschitz_with ‖s‖₊ ((•) s : β → β) :=
+lemma edist_smul_le (s : α) (x y : β) : edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y :=
+by simpa only [edist_nndist, ennreal.coe_mul] using ennreal.coe_le_coe.mpr (nndist_smul_le s x y)
+
+lemma lipschitz_with_smul (s : α) : lipschitz_with ‖s‖₊ ((•) s : β → β) :=
 lipschitz_with_iff_dist_le_mul.2 $ dist_smul_le _
 
 end seminormed_add_group
@@ -91,8 +94,10 @@ variables [module α β] [has_bounded_smul α β]
 lemma dist_smul₀ (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y :=
 by simp_rw [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 
-lemma nndist_smul₀ (s : α) (x y : β) :
-  nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
+lemma nndist_smul₀ (s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
 nnreal.eq $ dist_smul₀ s x y
 
+lemma edist_smul₀ (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]
+
 end normed_division_ring_module

src/analysis/normed_space/basic.lean

@@ -23,7 +23,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
 

src/analysis/normed_space/pointwise.lean

@@ -21,7 +21,59 @@ multiplication of bounded sets remain bounded.
 open metric set
 open_locale pointwise topology
 
-variables {𝕜 E : Type*} [normed_field 𝕜]
+variables {𝕜 E : Type*}
+
+section smul_zero_class
+variables [seminormed_add_comm_group 𝕜] [seminormed_add_comm_group E]
+variables [smul_zero_class 𝕜 E] [has_bounded_smul 𝕜 E]
+
+lemma ediam_smul_le (c : 𝕜) (s : set E) :
+  emetric.diam (c • s) ≤ ‖c‖₊ • emetric.diam s :=
+(lipschitz_with_smul c).ediam_image_le s
+
+end smul_zero_class
+
+section division_ring
+variables [normed_division_ring 𝕜] [seminormed_add_comm_group E]
+variables [module 𝕜 E] [has_bounded_smul 𝕜 E]
+
+lemma ediam_smul₀ (c : 𝕜) (s : set E) :
+  emetric.diam (c • s) = ‖c‖₊ • emetric.diam s :=
+begin
+  refine le_antisymm (ediam_smul_le c s) _,
+  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], },
+  { have := (lipschitz_with_smul c⁻¹).ediam_image_le (c • s),
+    rwa [← smul_eq_mul, ←ennreal.smul_def, set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
+      ennreal.le_inv_smul_iff (nnnorm_ne_zero_iff.mpr hc)] at this }
+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
+
+lemma inf_dist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : set E) (x : E) :
+  metric.inf_dist (c • x) (c • s) = ‖c‖ * metric.inf_dist x s :=
+by simp_rw [metric.inf_dist, inf_edist_smul₀ hc, ennreal.to_real_smul, nnreal.smul_def, coe_nnnorm,
+  smul_eq_mul]
+
+end division_ring
+
+variables [normed_field 𝕜]
 
 section seminormed_add_comm_group
 variables [seminormed_add_comm_group E] [normed_space 𝕜 E]

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`. -/
+protected 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`. -/
+protected 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 (ennreal.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/hausdorff_distance.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.specific_limits.basic
+import topology.metric_space.isometric_smul
 import topology.metric_space.isometry
 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 :=