feat(analysis/normed_space/pointwise): Addition of balls (#13381)

Adding two balls yields another ball.

Author: YaelDillies

src/analysis/normed/group/basic.lean

@@ -143,8 +143,10 @@ by simp [dist_eq_norm]
 @[simp] lemma dist_add_right (g₁ g₂ h : E) : dist (g₁ + h) (g₂ + h) = dist g₁ g₂ :=
 by simp [dist_eq_norm]
 
-@[simp] lemma dist_neg_neg (g h : E) : dist (-g) (-h) = dist g h :=
-by simp only [dist_eq_norm, neg_sub_neg, norm_sub_rev]
+lemma dist_neg (x y : E) : dist (-x) y = dist x (-y) :=
+by simp_rw [dist_eq_norm, ←norm_neg (-x - y), neg_sub, sub_neg_eq_add, add_comm]
+
+@[simp] lemma dist_neg_neg (g h : E) : dist (-g) (-h) = dist g h := by rw [dist_neg, neg_neg]
 
 @[simp] lemma dist_sub_left (g h₁ h₂ : E) : dist (g - h₁) (g - h₂) = dist h₁ h₂ :=
 by simp only [sub_eq_add_neg, dist_add_left, dist_neg_neg]
@@ -628,8 +630,8 @@ by simp [edist_dist]
 @[simp] lemma edist_add_right (g₁ g₂ h : E) : edist (g₁ + h) (g₂ + h) = edist g₁ g₂ :=
 by simp [edist_dist]
 
-@[simp] lemma edist_neg_neg (x y : E) : edist (-x) (-y) = edist x y :=
-by rw [edist_dist, dist_neg_neg, edist_dist]
+lemma edist_neg (x y : E) : edist (-x) y = edist x (-y) := by simp_rw [edist_dist, dist_neg]
+@[simp] lemma edist_neg_neg (x y : E) : edist (-x) (-y) = edist x y := by rw [edist_neg, neg_neg]
 
 @[simp] lemma edist_sub_left (g h₁ h₂ : E) : edist (g - h₁) (g - h₂) = edist h₁ h₂ :=
 by simp only [sub_eq_add_neg, edist_add_left, edist_neg_neg]

src/analysis/normed/group/pointwise.lean

@@ -3,11 +3,11 @@ 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 analysis.normed.group.add_torsor
 import topology.metric_space.hausdorff_distance
 
 /-!
-# Properties of pointwise addition of sets in normed groups.
+# Properties of pointwise addition of sets in normed groups
 
 We explore the relationships between pointwise addition of sets in normed groups, and the norm.
 Notably, we show that the sum of bounded sets remain bounded.
@@ -18,16 +18,14 @@ open_locale pointwise topological_space
 
 section semi_normed_group
 
-variables {E : Type*} [semi_normed_group E]
+variables {E : Type*} [semi_normed_group E] {ε δ : ℝ} {s t : set E} {x y : E}
 
-lemma bounded_iff_exists_norm_le {s : set E} :
-  bounded s ↔ ∃ R, ∀ x ∈ s, ∥x∥ ≤ R :=
+lemma bounded_iff_exists_norm_le : bounded s ↔ ∃ R, ∀ x ∈ s, ∥x∥ ≤ R :=
 by simp [subset_def, bounded_iff_subset_ball (0 : E)]
 
 alias bounded_iff_exists_norm_le ↔ metric.bounded.exists_norm_le _
 
-lemma metric.bounded.exists_pos_norm_le {s : set E} (hs : metric.bounded s) :
-  ∃ R > 0, ∀ x ∈ s, ∥x∥ ≤ R :=
+lemma metric.bounded.exists_pos_norm_le (hs : metric.bounded s) : ∃ R > 0, ∀ x ∈ s, ∥x∥ ≤ R :=
 begin
   obtain ⟨R₀, hR₀⟩ := hs.exists_norm_le,
   refine ⟨max R₀ 1, _, _⟩,
@@ -36,9 +34,7 @@ begin
   exact (hR₀ x hx).trans (le_max_left _ _),
 end
 
-lemma metric.bounded.add
-  {s t : set E} (hs : bounded s) (ht : bounded t) :
-  bounded (s + t) :=
+lemma metric.bounded.add (hs : bounded s) (ht : bounded t) : bounded (s + t) :=
 begin
   obtain ⟨Rs, hRs⟩ : ∃ (R : ℝ), ∀ x ∈ s, ∥x∥ ≤ R := hs.exists_norm_le,
   obtain ⟨Rt, hRt⟩ : ∃ (R : ℝ), ∀ x ∈ t, ∥x∥ ≤ R := ht.exists_norm_le,
@@ -48,46 +44,130 @@ begin
   ... ≤ Rs + Rt : add_le_add (hRs x hx) (hRt y hy)
 end
 
-@[simp] lemma singleton_add_ball (x y : E) (r : ℝ) :
-  {x} + ball y r = ball (x + y) r :=
+lemma metric.bounded.neg : bounded s → bounded (-s) :=
+by { simp_rw [bounded_iff_exists_norm_le, ←image_neg, ball_image_iff, norm_neg], exact id }
+
+lemma metric.bounded.sub (hs : bounded s) (ht : bounded t) : bounded (s - t) :=
+(sub_eq_add_neg _ _).symm.subst $ hs.add ht.neg
+
+section emetric
+open emetric
+
+lemma inf_edist_neg (x : E) (s : set E) : inf_edist (-x) s = inf_edist x (-s) :=
+eq_of_forall_le_iff $ λ r, by simp_rw [le_inf_edist, ←image_neg, ball_image_iff, edist_neg]
+
+@[simp] lemma inf_edist_neg_neg (x : E) (s : set E) : inf_edist (-x) (-s) = inf_edist x s :=
+by rw [inf_edist_neg, neg_neg]
+
+end emetric
+
+variables (ε δ s t x y)
+
+@[simp] lemma neg_thickening : -thickening δ s = thickening δ (-s) :=
+by { unfold thickening, simp_rw ←inf_edist_neg, refl }
+
+@[simp] lemma neg_cthickening : -cthickening δ s = cthickening δ (-s) :=
+by { unfold cthickening, simp_rw ←inf_edist_neg, refl }
+
+@[simp] lemma neg_ball : -ball x δ = ball (-x) δ :=
+by { unfold metric.ball, simp_rw ←dist_neg, refl }
+
+@[simp] lemma neg_closed_ball : -closed_ball x δ = closed_ball (-x) δ :=
+by { unfold metric.closed_ball, simp_rw ←dist_neg, refl }
+
+lemma singleton_add_ball : {x} + ball y δ = ball (x + y) δ :=
 by simp only [preimage_add_ball, image_add_left, singleton_add, sub_neg_eq_add, add_comm y x]
 
-@[simp] lemma ball_add_singleton (x y : E) (r : ℝ) :
-  ball x r + {y} = ball (x + y) r :=
-by simp [add_comm _ {y}, add_comm y]
+lemma singleton_sub_ball : {x} - ball y δ = ball (x - y) δ :=
+by simp_rw [sub_eq_add_neg, neg_ball, singleton_add_ball]
+
+lemma ball_add_singleton : ball x δ + {y} = ball (x + y) δ :=
+by rw [add_comm, singleton_add_ball, add_comm y]
 
-lemma singleton_add_ball_zero (x : E) (r : ℝ) :
-  {x} + ball 0 r = ball x r :=
-by simp
+lemma ball_sub_singleton : ball x δ - {y} = ball (x - y) δ :=
+by simp_rw [sub_eq_add_neg, neg_singleton, ball_add_singleton]
 
-lemma ball_zero_add_singleton (x : E) (r : ℝ) :
-  ball 0 r + {x} = ball x r :=
-by simp
+lemma singleton_add_ball_zero : {x} + ball 0 δ = ball x δ := by simp
+lemma singleton_sub_ball_zero : {x} - ball 0 δ = ball x δ := by simp [singleton_sub_ball]
+lemma ball_zero_add_singleton : ball 0 δ + {x} = ball x δ := by simp [ball_add_singleton]
+lemma ball_zero_sub_singleton : ball 0 δ - {x} = ball (-x) δ := by simp [ball_sub_singleton]
+lemma vadd_ball_zero : x +ᵥ ball 0 δ = ball x δ := by simp
 
-@[simp] lemma singleton_add_closed_ball (x y : E) (r : ℝ) :
-  {x} + closed_ball y r = closed_ball (x + y) r :=
+@[simp] lemma singleton_add_closed_ball : {x} + closed_ball y δ = closed_ball (x + y) δ :=
 by simp only [add_comm y x, preimage_add_closed_ball, image_add_left, singleton_add, sub_neg_eq_add]
 
-@[simp] lemma closed_ball_add_singleton (x y : E) (r : ℝ) :
-  closed_ball x r + {y} = closed_ball (x + y) r :=
+@[simp] lemma singleton_sub_closed_ball : {x} - closed_ball y δ = closed_ball (x - y) δ :=
+by simp_rw [sub_eq_add_neg, neg_closed_ball, singleton_add_closed_ball]
+
+@[simp] lemma closed_ball_add_singleton : closed_ball x δ + {y} = closed_ball (x + y) δ :=
 by simp [add_comm _ {y}, add_comm y]
 
-lemma singleton_add_closed_ball_zero (x : E) (r : ℝ) :
-  {x} + closed_ball 0 r = closed_ball x r :=
-by simp
+@[simp] lemma closed_ball_sub_singleton : closed_ball x δ - {y} = closed_ball (x - y) δ :=
+by simp [sub_eq_add_neg]
 
-lemma closed_ball_zero_add_singleton (x : E) (r : ℝ) :
-  closed_ball 0 r + {x} = closed_ball x r :=
-by simp
+lemma singleton_add_closed_ball_zero : {x} + closed_ball 0 δ = closed_ball x δ := by simp
+lemma singleton_sub_closed_ball_zero : {x} - closed_ball 0 δ = closed_ball x δ := by simp
+lemma closed_ball_zero_add_singleton : closed_ball 0 δ + {x} = closed_ball x δ := by simp
+lemma closed_ball_zero_sub_singleton : closed_ball 0 δ - {x} = closed_ball (-x) δ := by simp
+@[simp] lemma vadd_closed_ball_zero : x +ᵥ closed_ball 0 δ = closed_ball x δ := 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 :=
+lemma add_ball_zero : s + ball 0 δ = thickening δ s :=
 begin
-  rw hs.cthickening_eq_bUnion_closed_ball hr,
+  rw thickening_eq_bUnion_ball,
+  convert Union₂_add (λ x (_ : x ∈ s), {x}) (ball (0 : E) δ),
+  exact s.bUnion_of_singleton.symm,
+  ext x y,
+  simp_rw [singleton_add_ball, add_zero],
+end
+
+lemma sub_ball_zero : s - ball 0 δ = thickening δ s := by simp [sub_eq_add_neg, add_ball_zero]
+lemma ball_add_zero : ball 0 δ + s = thickening δ s := by rw [add_comm, add_ball_zero]
+lemma ball_sub_zero : ball 0 δ - s = thickening δ (-s) := by simp [sub_eq_add_neg, ball_add_zero]
+
+@[simp] lemma add_ball : s + ball x δ = x +ᵥ thickening δ s :=
+by rw [←vadd_ball_zero, add_vadd_comm, add_ball_zero]
+
+@[simp] lemma sub_ball : s - ball x δ = -x +ᵥ thickening δ s := by simp [sub_eq_add_neg]
+@[simp] lemma ball_add : ball x δ + s = x +ᵥ thickening δ s := by rw [add_comm, add_ball]
+@[simp] lemma ball_sub : ball x δ - s = x +ᵥ thickening δ (-s) := by simp [sub_eq_add_neg]
+
+variables {ε δ s t x y}
+
+lemma is_compact.add_closed_ball_zero (hs : is_compact s) (hδ : 0 ≤ δ) :
+  s + closed_ball 0 δ = cthickening δ s :=
+begin
+  rw hs.cthickening_eq_bUnion_closed_ball hδ,
   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
 
+lemma is_compact.sub_closed_ball_zero (hs : is_compact s) (hδ : 0 ≤ δ) :
+  s - closed_ball 0 δ = cthickening δ s :=
+by simp [sub_eq_add_neg, hs.add_closed_ball_zero hδ]
+
+lemma is_compact.closed_ball_zero_add (hs : is_compact s) (hδ : 0 ≤ δ) :
+  closed_ball 0 δ + s = cthickening δ s :=
+by rw [add_comm, hs.add_closed_ball_zero hδ]
+
+lemma is_compact.closed_ball_zero_sub (hs : is_compact s) (hδ : 0 ≤ δ) :
+  closed_ball 0 δ - s = cthickening δ (-s) :=
+by simp [sub_eq_add_neg, add_comm, hs.neg.add_closed_ball_zero hδ]
+
+lemma is_compact.add_closed_ball (hs : is_compact s) (hδ : 0 ≤ δ) (x : E) :
+  s + closed_ball x δ = x +ᵥ cthickening δ s :=
+by rw [←vadd_closed_ball_zero, add_vadd_comm, hs.add_closed_ball_zero hδ]
+
+lemma is_compact.sub_closed_ball (hs : is_compact s) (hδ : 0 ≤ δ) (x : E) :
+  s - closed_ball x δ = -x +ᵥ cthickening δ s :=
+by simp [sub_eq_add_neg, add_comm, hs.add_closed_ball hδ]
+
+lemma is_compact.closed_ball_add (hs : is_compact s) (hδ : 0 ≤ δ) (x : E) :
+  closed_ball x δ + s = x +ᵥ cthickening δ s :=
+by rw [add_comm, hs.add_closed_ball hδ]
+
+lemma is_compact.closed_ball_sub (hs : is_compact s) (hδ : 0 ≤ δ) (x : E) :
+  closed_ball x δ + s = x +ᵥ cthickening δ s :=
+by simp [sub_eq_add_neg, add_comm, hs.closed_ball_add hδ]
+
 end semi_normed_group

src/analysis/normed_space/pointwise.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import analysis.normed.group.pointwise
-import analysis.normed.group.add_torsor
 import analysis.normed_space.basic
-import topology.metric_space.hausdorff_distance
 
 /-!
 # Properties of pointwise scalar multiplication of sets in normed spaces.
@@ -87,14 +85,6 @@ begin
   simpa only [this, dist_eq_norm, add_sub_cancel', mem_closed_ball] using I,
 end
 
-/-- Any ball is the image of a ball centered at the origin under a shift. -/
-lemma vadd_ball_zero (x : E) (r : ℝ) : x +ᵥ ball 0 r = ball x r :=
-by rw [vadd_ball, vadd_eq_add, add_zero]
-
-/-- Any closed ball is the image of a closed ball centered at the origin under a shift. -/
-lemma vadd_closed_ball_zero (x : E) (r : ℝ) : x +ᵥ closed_ball 0 r = closed_ball x r :=
-by rw [vadd_closed_ball, vadd_eq_add, add_zero]
-
 variables [normed_space ℝ E] {x y z : E} {δ ε : ℝ}
 
 /-- In a real normed space, the image of the unit ball under scalar multiplication by a positive
@@ -264,6 +254,58 @@ end
   exact tsub_le_iff_right.2,
 end
 
+@[simp] lemma thickening_ball (hε : 0 < ε) (hδ : 0 < δ) (x : E) :
+  thickening ε (ball x δ) = ball x (ε + δ) :=
+by rw [←thickening_singleton, thickening_thickening hε hδ, thickening_singleton]; apply_instance
+
+@[simp] lemma thickening_closed_ball (hε : 0 < ε) (hδ : 0 ≤ δ) (x : E) :
+  thickening ε (closed_ball x δ) = ball x (ε + δ) :=
+by rw [←cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton];
+  apply_instance
+
+@[simp] lemma cthickening_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) :
+  cthickening ε (ball x δ) = closed_ball x (ε + δ) :=
+by rw [←thickening_singleton, cthickening_thickening hε hδ,
+  cthickening_singleton _ (add_nonneg hε hδ.le)]; apply_instance
+
+@[simp] lemma cthickening_closed_ball (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (x : E) :
+  cthickening ε (closed_ball x δ) = closed_ball x (ε + δ) :=
+by rw [←cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
+  cthickening_singleton _ (add_nonneg hε hδ)]; apply_instance
+
+lemma ball_add_ball (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
+  ball a ε + ball b δ = ball (a + b) (ε + δ) :=
+by rw [ball_add, thickening_ball hε hδ, vadd_ball, vadd_eq_add]; apply_instance
+
+lemma ball_sub_ball (hε : 0 < ε) (hδ : 0 < δ) (a b : E) :
+  ball a ε - ball b δ = ball (a - b) (ε + δ) :=
+by simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]
+
+lemma ball_add_closed_ball (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) :
+  ball a ε + closed_ball b δ = ball (a + b) (ε + δ) :=
+by rw [ball_add, thickening_closed_ball hε hδ, vadd_ball, vadd_eq_add]; apply_instance
+
+lemma ball_sub_closed_ball (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) :
+  ball a ε - closed_ball b δ = ball (a - b) (ε + δ) :=
+by simp_rw [sub_eq_add_neg, neg_closed_ball, ball_add_closed_ball hε hδ]
+
+lemma closed_ball_add_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) :
+  closed_ball a ε + ball b δ = ball (a + b) (ε + δ) :=
+by rw [add_comm, ball_add_closed_ball hδ hε, add_comm, add_comm δ]; apply_instance
+
+lemma closed_ball_sub_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) :
+  closed_ball a ε - ball b δ = ball (a - b) (ε + δ) :=
+by simp_rw [sub_eq_add_neg, neg_ball, closed_ball_add_ball hε hδ]
+
+lemma closed_ball_add_closed_ball [proper_space E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
+  closed_ball a ε + closed_ball b δ = closed_ball (a + b) (ε + δ) :=
+by rw [(is_compact_closed_ball _ _).add_closed_ball hδ, cthickening_closed_ball hδ hε,
+  vadd_closed_ball, vadd_eq_add, add_comm, add_comm δ]; apply_instance
+
+lemma closed_ball_sub_closed_ball [proper_space E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
+  closed_ball a ε - closed_ball b δ = closed_ball (a - b) (ε + δ) :=
+by simp_rw [sub_eq_add_neg, neg_closed_ball, closed_ball_add_closed_ball hε hδ]
+
 end semi_normed_group
 
 section normed_group

src/data/set/pointwise.lean

@@ -503,7 +503,7 @@ lemma inv_subset_inv : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :=
 
 @[to_additive] lemma inv_subset : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹ := by { rw [← inv_subset_inv, inv_inv] }
 
-@[to_additive] lemma inv_singleton (a : α) : ({a} : set α)⁻¹ = {a⁻¹} :=
+@[simp, to_additive] lemma inv_singleton (a : α) : ({a} : set α)⁻¹ = {a⁻¹} :=
 by rw [←image_inv, image_singleton]
 
 open mul_opposite

src/measure_theory/function/jacobian.lean

@@ -297,7 +297,7 @@ begin
       (𝓝[>] 0) (𝓝 (μ (A '' (closed_ball 0 1)))),
     { apply L0.congr' _,
       filter_upwards [self_mem_nhds_within] with r hr,
-      rw [HC.cthickening_eq_add_closed_ball (le_of_lt hr), add_comm] },
+      rw [←HC.add_closed_ball_zero (le_of_lt hr), add_comm] },
     have L2 : tendsto (λ ε, μ (closed_ball 0 ε + A '' (closed_ball 0 1)))
       (𝓝[>] 0) (𝓝 (d * μ (closed_ball 0 1))),
     { convert L1,