feat(analysis/normed/group/pointwise): the closed thickening of a compact set is the addition of a closed ball. (#11528)

Author: sgouezel

src/analysis/normed/group/pointwise.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-
 import analysis.normed.group.basic
+import topology.metric_space.hausdorff_distance
 
 /-!
 # Properties of pointwise addition of sets in normed groups.
@@ -80,4 +80,14 @@ lemma closed_ball_zero_add_singleton (x : E) (r : ℝ) :
   closed_ball 0 r + {x} = closed_ball x r :=
 by simp
 
+lemma is_compact.cthickening_eq_add_closed_ball
+  {s : set E} (hs : is_compact s) {r : ℝ} (hr : 0 ≤ r) :
+  cthickening r s = s + closed_ball 0 r :=
+begin
+  rw hs.cthickening_eq_bUnion_closed_ball hr,
+  ext x,
+  simp only [mem_add, dist_eq_norm, exists_prop, mem_Union, mem_closed_ball,
+    exists_and_distrib_left, mem_closed_ball_zero_iff, ← eq_sub_iff_add_eq', exists_eq_right],
+end
+
 end semi_normed_group

src/topology/metric_space/hausdorff_distance.lean

@@ -858,6 +858,10 @@ begin
   simp_rw [mem_thickening_iff_exists_edist_lt, key_iff],
 end
 
+@[simp] lemma thickening_singleton (δ : ℝ) (x : X) :
+  thickening δ ({x} : set X) = ball x δ :=
+by { ext, simp [mem_thickening_iff] }
+
 /-- The (open) `δ`-thickening `thickening δ E` of a subset `E` in a metric space equals the
 union of balls of radius `δ` centered at points of `E`. -/
 lemma thickening_eq_bUnion_ball {δ : ℝ} {E : set X} :
@@ -927,6 +931,20 @@ lemma cthickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α)
   cthickening δ₁ E ⊆ cthickening δ₂ E :=
 preimage_mono (Iic_subset_Iic.mpr (ennreal.of_real_le_of_real hle))
 
+@[simp] lemma cthickening_singleton {α : Type*} [pseudo_metric_space α]
+  (x : α) {δ : ℝ} (hδ : 0 ≤ δ) :
+  cthickening δ ({x} : set α) = closed_ball x δ :=
+by { ext y, simp [cthickening, edist_dist, ennreal.of_real_le_of_real_iff hδ] }
+
+lemma closed_ball_subset_cthickening_singleton {α : Type*} [pseudo_metric_space α]
+  (x : α) (δ : ℝ) :
+  closed_ball x δ ⊆ cthickening δ ({x} : set α) :=
+begin
+  rcases lt_or_le δ 0 with hδ|hδ,
+  { simp only [closed_ball_eq_empty.mpr hδ, empty_subset] },
+  { simp only [cthickening_singleton x hδ] }
+end
+
 /-- The closed thickening `cthickening δ E` with a fixed thickening radius `δ` is
 an increasing function of the subset `E`. -/
 lemma cthickening_subset_of_subset (δ : ℝ) {E₁ E₂ : set α} (h : E₁ ⊆ E₂) :
@@ -1096,6 +1114,34 @@ begin
   exact continuous_inf_edist.frontier_preimage_subset (Iic (ennreal.of_real δ)),
 end
 
+/-- The closed ball of radius `δ` centered at a point of `E` is included in the closed
+thickening of `E`. -/
+lemma closed_ball_subset_cthickening {α : Type*} [pseudo_metric_space α]
+  {x : α} {E : set α} (hx : x ∈ E) (δ : ℝ) :
+  closed_ball x δ ⊆ cthickening δ E :=
+begin
+  refine (closed_ball_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ _),
+  simpa using hx,
+end
+
+/-- The closed thickening of a compact set `E` is the union of the balls `closed_ball x δ` over
+`x ∈ E`. -/
+lemma _root_.is_compact.cthickening_eq_bUnion_closed_ball
+  {α : Type*} [pseudo_metric_space α] {δ : ℝ} {E : set α} (hE : is_compact E) (hδ : 0 ≤ δ) :
+  cthickening δ E = ⋃ x ∈ E, closed_ball x δ :=
+begin
+  rcases eq_empty_or_nonempty E with rfl|hne,
+  { simp only [cthickening_empty, Union_false, Union_empty] },
+  refine subset.antisymm (λ x hx, _) (bUnion_subset (λ x hx, closed_ball_subset_cthickening hx _)),
+  obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, emetric.inf_edist x E = edist x y :=
+    hE.exists_inf_edist_eq_edist hne _,
+  have D1 : edist x y ≤ ennreal.of_real δ := (le_of_eq hy.symm).trans hx,
+  have D2 : dist x y ≤ δ,
+  { rw edist_dist at D1,
+    exact (ennreal.of_real_le_of_real_iff hδ).1 D1 },
+  exact mem_bUnion yE D2,
+end
+
 end cthickening --section
 
 end metric --namespace