feat(topology/metric/hausdorff_distance): more properties of cthicken…

…ing (#10808)

src/topology/metric_space/basic.lean

@@ -1094,6 +1094,19 @@ lemma tendsto_iff_of_dist {ι : Type*} {f₁ f₂ : ι → α} {p : filter ι} {
   tendsto f₁ p (𝓝 a) ↔ tendsto f₂ p (𝓝 a) :=
 uniform.tendsto_congr $ tendsto_uniformity_iff_dist_tendsto_zero.2 h
 
+/-- If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball
+`closed_ball x r` is contained in `u`. -/
+lemma eventually_closed_ball_subset {x : α} {u : set α} (hu : u ∈ 𝓝 x) :
+  ∀ᶠ r in 𝓝 (0 : ℝ), closed_ball x r ⊆ u :=
+begin
+  obtain ⟨ε, εpos, hε⟩ : ∃ ε (hε : 0 < ε), closed_ball x ε ⊆ u :=
+    nhds_basis_closed_ball.mem_iff.1 hu,
+  have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos,
+  filter_upwards [this],
+  assume r hr,
+  exact subset.trans (closed_ball_subset_closed_ball hr) hε,
+end
+
 end real
 
 section cauchy_seq
@@ -1784,6 +1797,23 @@ bounded_range_of_tendsto_cofinite_uniformity $
 lemma bounded_of_compact_space [compact_space α] : bounded s :=
 compact_univ.bounded.mono (subset_univ _)
 
+lemma bounded_range_of_tendsto {α : Type*} [pseudo_metric_space α] (u : ℕ → α) {x : α}
+  (hu : tendsto u at_top (𝓝 x)) :
+  bounded (range u) :=
+begin
+  classical,
+  obtain ⟨N, hN⟩ : ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → dist (u n) x < 1 :=
+    metric.tendsto_at_top.1 hu 1 zero_lt_one,
+  have : range u ⊆ (finset.range N).image u ∪ ball x 1,
+  { refine range_subset_iff.2 (λ n, _),
+    rcases lt_or_le n N with h|h,
+    { left,
+      simp only [mem_image, finset.mem_range, finset.mem_coe, finset.coe_image],
+      exact ⟨n, h, rfl⟩ },
+    { exact or.inr (mem_ball.2 (hN n h)) } },
+  exact bounded.mono this ((finset.finite_to_set _).bounded.union bounded_ball)
+end
+
 lemma is_compact_of_is_closed_bounded [proper_space α] (hc : is_closed s) (hb : bounded s) :
   is_compact s :=
 begin

src/topology/metric_space/hausdorff_distance.lean

@@ -163,6 +163,15 @@ begin
     exact ⟨n, hn.le⟩ },
 end
 
+lemma _root_.is_compact.exists_inf_edist_eq_edist (hs : is_compact s) (hne : s.nonempty) :
+  ∃ y ∈ s, inf_edist x s = edist x y :=
+begin
+  have A : continuous (λ y, edist x y) := continuous_const.edist continuous_id,
+  obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, ∀ z, z ∈ s → edist x y ≤ edist x z :=
+    hs.exists_forall_le hne A.continuous_on,
+  exact ⟨y, ys, le_antisymm (inf_edist_le_edist_of_mem ys) (by rwa le_inf_edist)⟩
+end
+
 end inf_edist --section
 
 /-! ### The Hausdorff distance as a function into `ℝ≥0∞`. -/
@@ -791,7 +800,7 @@ begin
     exact lt_of_le_of_lt (@inf_edist_le_edist_of_mem _ _ x _ _ hzE) hxz, },
 end
 
-variables {X : Type u} [metric_space X]
+variables {X : Type u} [pseudo_metric_space X]
 
 /-- A point in a metric space belongs to the (open) `δ`-thickening of a subset `E` if and only if
 it is at distance less than `δ` from some point of `E`. -/
@@ -814,6 +823,18 @@ lemma thickening_eq_bUnion_ball {δ : ℝ} {E : set X} :
   thickening δ E = ⋃ x ∈ E, ball x δ :=
 by { ext x, rw mem_bUnion_iff, exact mem_thickening_iff E x, }
 
+lemma bounded.thickening {δ : ℝ} {E : set X} (h : bounded E) :
+  bounded (thickening δ E) :=
+begin
+  refine bounded_iff_mem_bounded.2 (λ x hx, _),
+  rcases h.subset_ball x with ⟨R, hR⟩,
+  refine (bounded_iff_subset_ball x).2 ⟨R + δ, _⟩,
+  assume y hy,
+  rcases (mem_thickening_iff _ _).1 hy with ⟨z, zE, hz⟩,
+  calc dist y x ≤ dist z x + dist y z : by { rw add_comm, exact dist_triangle _ _ _ }
+  ... ≤ R + δ : add_le_add (hR zE) hz.le
+end
+
 end thickening --section
 
 section cthickening
@@ -826,7 +847,20 @@ open emetric
 of those points that are at infimum distance at most `δ` from `E`. -/
 def cthickening (δ : ℝ) (E : set α) : set α := {x : α | inf_edist x E ≤ ennreal.of_real δ}
 
-/-- The closed thickening equals the preimage of a closed interval under `inf_edist`. -/
+lemma mem_cthickening_of_edist_le (x y : α) (δ : ℝ) (E : set α) (h : y ∈ E)
+  (h' : edist x y ≤ ennreal.of_real δ) :
+  x ∈ cthickening δ E :=
+(inf_edist_le_edist_of_mem h).trans h'
+
+lemma mem_cthickening_of_dist_le {α : Type*} [pseudo_metric_space α]
+  (x y : α) (δ : ℝ) (E : set α) (h : y ∈ E) (h' : dist x y ≤ δ) :
+  x ∈ cthickening δ E :=
+begin
+  apply mem_cthickening_of_edist_le x y δ E h,
+  rw edist_dist,
+  exact ennreal.of_real_le_of_real h',
+end
+
 lemma cthickening_eq_preimage_inf_edist (δ : ℝ) (E : set α) :
   cthickening δ E = (λ x, inf_edist x E) ⁻¹' (Iic (ennreal.of_real δ)) := rfl
 
@@ -878,6 +912,15 @@ lemma thickening_subset_cthickening_of_le {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ 
   thickening δ₁ E ⊆ cthickening δ₂ E :=
 (thickening_subset_cthickening δ₁ E).trans (cthickening_mono hle E)
 
+lemma bounded.cthickening {α : Type*} [pseudo_metric_space α] {δ : ℝ} {E : set α} (h : bounded E) :
+  bounded (cthickening δ E) :=
+begin
+  have : bounded (thickening (max (δ + 1) 1) E) := h.thickening,
+  apply bounded.mono _ this,
+  exact cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _))
+    ((lt_add_one _).trans_le (le_max_left _ _)) _
+end
+
 lemma thickening_subset_interior_cthickening (δ : ℝ) (E : set α) :
   thickening δ E ⊆ interior (cthickening δ E) :=
 (subset_interior_iff_open.mpr (is_open_thickening)).trans