feat(topology/metric_space): diameter of pointwise zero and addition (#…

…19028)

src/analysis/normed/group/pointwise.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import analysis.normed.group.basic
 import topology.metric_space.hausdorff_distance
+import topology.metric_space.isometric_smul
 
 /-!
 # Properties of pointwise addition of sets in normed groups
@@ -24,6 +25,7 @@ variables {E : Type*}
 section seminormed_group
 variables [seminormed_group E] {ε δ : ℝ} {s t : set E} {x y : E}
 
+-- note: we can't use `lipschitz_on_with.bounded_image2` here without adding `[isometric_smul E E]`
 @[to_additive] lemma metric.bounded.mul (hs : bounded s) (ht : bounded t) : bounded (s * t) :=
 begin
   obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le',
@@ -33,6 +35,10 @@ begin
   exact norm_mul_le_of_le (hRs x hx) (hRt y hy),
 end
 
+@[to_additive] lemma metric.bounded.of_mul (hst : bounded (s * t)) :
+  bounded s ∨ bounded t :=
+antilipschitz_with.bounded_of_image2_left _ (λ x, (isometry_mul_right x).antilipschitz) hst
+
 @[to_additive] lemma metric.bounded.inv : bounded s → bounded s⁻¹ :=
 by { simp_rw [bounded_iff_forall_norm_le', ←image_inv, ball_image_iff, norm_inv'], exact id }
 
@@ -55,6 +61,13 @@ 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 ediam_mul_le (x y : set E) :
+  emetric.diam (x * y) ≤ emetric.diam x + emetric.diam y :=
+(lipschitz_on_with.ediam_image2_le (*) _ _
+    (λ _ _, (isometry_mul_right _).lipschitz.lipschitz_on_with _)
+    (λ _ _, (isometry_mul_left _).lipschitz.lipschitz_on_with _)).trans_eq $
+  by simp only [ennreal.coe_one, one_mul]
+
 end emetric
 
 variables (ε δ s t x y)

src/topology/metric_space/antilipschitz.lean

@@ -192,7 +192,8 @@ namespace antilipschitz_with
 
 open metric
 
-variables [pseudo_metric_space α] [pseudo_metric_space β] {K : ℝ≥0} {f : α → β}
+variables [pseudo_metric_space α] [pseudo_metric_space β] [pseudo_metric_space γ]
+variables {K : ℝ≥0} {f : α → β}
 
 lemma bounded_preimage (hf : antilipschitz_with K f)
   {s : set β} (hs : bounded s) :
@@ -219,6 +220,28 @@ begin
   exact (hf.image_preimage _).symm
 end
 
+lemma bounded_of_image2_left (f : α → β → γ) {K₁ : ℝ≥0}
+  (hf : ∀ b, antilipschitz_with K₁ (λ a, f a b))
+  {s : set α} {t : set β} (hst : bounded (set.image2 f s t)) :
+  bounded s ∨ bounded t :=
+begin
+  contrapose! hst,
+  obtain ⟨b, hb⟩ : t.nonempty := nonempty_of_unbounded hst.2,
+  have : ¬bounded (set.image2 f s {b}),
+  { intro h,
+    apply hst.1,
+    rw set.image2_singleton_right at h,
+    replace h := (hf b).bounded_preimage h,
+    refine h.mono (subset_preimage_image _ _) },
+  exact mt (bounded.mono (image2_subset subset.rfl (singleton_subset_iff.mpr hb))) this,
+end
+
+lemma bounded_of_image2_right {f : α → β → γ} {K₂ : ℝ≥0}
+  (hf : ∀ a, antilipschitz_with K₂ (f a))
+  {s : set α} {t : set β} (hst : bounded (set.image2 f s t)) :
+  bounded s ∨ bounded t :=
+or.symm $ bounded_of_image2_left (flip f) hf $ image2_swap f s t ▸ hst
+
 end antilipschitz_with
 
 lemma lipschitz_with.to_right_inverse [pseudo_emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}

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*}
@@ -2171,6 +2171,13 @@ end
 @[simp] lemma bounded_empty : bounded (∅ : set α) :=
 ⟨0, by simp⟩
 
+lemma nonempty_of_unbounded (h : ¬ bounded s) : s.nonempty :=
+begin
+  rw nonempty_iff_ne_empty,
+  rintro rfl,
+  exact h bounded_empty
+end
+
 lemma bounded_iff_mem_bounded : bounded s ↔ ∀ x ∈ s, bounded s :=
 ⟨λ h _ _, h, λ H,
   s.eq_empty_or_nonempty.elim
@@ -2453,6 +2460,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/lipschitz.lean

@@ -465,6 +465,20 @@ protected lemma comp {g : β → γ} {t : set β} {Kg : ℝ≥0} (hg : lipschitz
   lipschitz_on_with (Kg * K) (g ∘ f) s :=
 lipschitz_on_with_iff_restrict.mpr $ hg.to_restrict.comp (hf.to_restrict_maps_to hmaps)
 
+lemma ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0}
+  (s : set α) (t : set β)
+  (hf₁ : ∀ b ∈ t, lipschitz_on_with K₁ (λ a, f a b) s)
+  (hf₂ : ∀ a ∈ s, lipschitz_on_with K₂ (f a) t) :
+  emetric.diam (set.image2 f s t) ≤ ↑K₁ * emetric.diam s + ↑K₂ * emetric.diam t :=
+begin
+  apply emetric.diam_le,
+  rintros _ ⟨a₁, b₁, ha₁, hb₁, rfl⟩ _  ⟨a₂, b₂, ha₂, hb₂, rfl⟩,
+  refine (edist_triangle _ (f a₂ b₁) _).trans _,
+  exact add_le_add
+    ((hf₁ b₁ hb₁ ha₁ ha₂).trans $ ennreal.mul_left_mono $ emetric.edist_le_diam_of_mem ha₁ ha₂)
+    ((hf₂ a₂ ha₂ hb₁ hb₂).trans $ ennreal.mul_left_mono $ emetric.edist_le_diam_of_mem hb₁ hb₂),
+end
+
 end emetric
 
 section metric
@@ -512,6 +526,17 @@ protected lemma iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
   lipschitz_on_with K f s ↔ ∀ (x ∈ s) (y ∈ s), f x ≤ f y + K * dist x y :=
 ⟨lipschitz_on_with.le_add_mul, lipschitz_on_with.of_le_add_mul K⟩
 
+lemma bounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0}
+  {s : set α} {t : set β} (hs : metric.bounded s) (ht : metric.bounded t)
+  (hf₁ : ∀ b ∈ t, lipschitz_on_with K₁ (λ a, f a b) s)
+  (hf₂ : ∀ a ∈ s, lipschitz_on_with K₂ (f a) t) :
+  metric.bounded (set.image2 f s t) :=
+metric.bounded_iff_ediam_ne_top.2 $ ne_top_of_le_ne_top
+  (ennreal.add_ne_top.mpr ⟨
+    ennreal.mul_ne_top ennreal.coe_ne_top hs.ediam_ne_top,
+    ennreal.mul_ne_top ennreal.coe_ne_top ht.ediam_ne_top⟩)
+  (ediam_image2_le _ _ _ hf₁ hf₂)
+
 end metric
 
 end lipschitz_on_with