feat(analysis/normed_space/pointwise): Balls disjointness (#13379)

Two balls in a real normed space are disjoint iff the sum of their radii is less than the distance between their centers.

Author: YaelDillies

src/algebra/module/basic.lean

@@ -72,6 +72,10 @@ instance add_comm_monoid.nat_module : module ℕ M :=
   add_smul := λ r s x, add_nsmul x r s }
 
 theorem add_smul : (r + s) • x = r • x + s • x := module.add_smul r s x
+
+lemma convex.combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x :=
+by rw [←add_smul, h, one_smul]
+
 variables (R)
 
 theorem two_smul : (2 : R) • x = x + x := by rw [bit0, add_smul, one_smul]
@@ -80,7 +84,7 @@ theorem two_smul' : (2 : R) • x = bit0 x := two_smul R x
 
 @[simp] lemma inv_of_two_smul_add_inv_of_two_smul [invertible (2 : R)] (x : M) :
   (⅟2 : R) • x + (⅟2 : R) • x = x :=
-by rw [←add_smul, inv_of_two_add_inv_of_two, one_smul]
+convex.combo_self inv_of_two_add_inv_of_two _
 
 /-- Pullback a `module` structure along an injective additive monoid homomorphism.
 See note [reducible non-instances]. -/

src/algebra/order/ring.lean

@@ -177,6 +177,12 @@ ordered_semiring.mul_lt_mul_of_pos_left a b c h₁ h₂
 lemma mul_lt_mul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c :=
 ordered_semiring.mul_lt_mul_of_pos_right a b c h₁ h₂
 
+lemma mul_lt_of_lt_one_left (hb : 0 < b) (ha : a < 1) : a * b < b :=
+(mul_lt_mul_of_pos_right ha hb).trans_le (one_mul _).le
+
+lemma mul_lt_of_lt_one_right (ha : 0 < a) (hb : b < 1) : a * b < a :=
+(mul_lt_mul_of_pos_left hb ha).trans_le (mul_one _).le
+
 -- See Note [decidable namespace]
 protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
   (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=

src/analysis/convex/basic.lean

@@ -145,9 +145,6 @@ begin
   exact h (mem_open_segment_of_ne_left_right 𝕜 hxz hyz hz),
 end
 
-lemma convex.combo_self {a b : 𝕜} (h : a + b = 1) (x : E) : a • x + b • x = x :=
-by rw [←add_smul, h, one_smul]
-
 end module
 end ordered_semiring
 

src/analysis/normed_space/pointwise.lean

@@ -1,7 +1,7 @@
 /-
 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
+Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import analysis.normed.group.pointwise
 import analysis.normed.group.add_torsor
@@ -95,13 +95,104 @@ by rw [vadd_ball, vadd_eq_add, add_zero]
 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]
+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
 constant `r` is the ball of radius `r`. -/
 lemma smul_unit_ball_of_pos {r : ℝ} (hr : 0 < r) : r • ball 0 1 = ball (0 : E) r :=
 by rw [smul_unit_ball hr.ne', real.norm_of_nonneg hr.le]
 
+-- This is also true for `ℚ`-normed spaces
+lemma exists_dist_eq (x z : E) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
+  ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z :=
+begin
+  use a • x + b • z,
+  nth_rewrite 0 [←one_smul ℝ x],
+  nth_rewrite 3 [←one_smul ℝ z],
+  simp [dist_eq_norm, ←hab, add_smul, ←smul_sub, norm_smul_of_nonneg, ha, hb],
+end
+
+lemma exists_dist_le_le (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (h : dist x z ≤ ε + δ) :
+  ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε :=
+begin
+  obtain rfl | hε' := hε.eq_or_lt,
+  { exact ⟨z, by rwa zero_add at h, (dist_self _).le⟩ },
+  have hεδ := add_pos_of_pos_of_nonneg hε' hδ,
+  refine (exists_dist_eq x z (div_nonneg hε $ add_nonneg hε hδ) (div_nonneg hδ $ add_nonneg hε hδ) $
+    by rw [←add_div, div_self hεδ.ne']).imp (λ y hy, _),
+  rw [hy.1, hy.2, div_mul_comm', div_mul_comm' ε],
+  rw ←div_le_one hεδ at h,
+  exact ⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma exists_dist_le_lt (hδ : 0 ≤ δ) (hε : 0 < ε) (h : dist x z < ε + δ) :
+  ∃ y, dist x y ≤ δ ∧ dist y z < ε :=
+begin
+  refine (exists_dist_eq x z (div_nonneg hε.le $ add_nonneg hε.le hδ) (div_nonneg hδ $ add_nonneg
+    hε.le hδ) $ by rw [←add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']).imp (λ y hy, _),
+  rw [hy.1, hy.2, div_mul_comm', div_mul_comm' ε],
+  rw ←div_lt_one (add_pos_of_pos_of_nonneg hε hδ) at h,
+  exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma exists_dist_lt_le (hδ : 0 < δ) (hε : 0 ≤ ε) (h : dist x z < ε + δ) :
+  ∃ y, dist x y < δ ∧ dist y z ≤ ε :=
+begin
+  obtain ⟨y, yz, xy⟩ := exists_dist_le_lt hε hδ
+    (show dist z x < δ + ε, by simpa only [dist_comm, add_comm] using h),
+  exact ⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma exists_dist_lt_lt (hδ : 0 < δ) (hε : 0 < ε) (h : dist x z < ε + δ) :
+  ∃ y, dist x y < δ ∧ dist y z < ε :=
+begin
+  refine (exists_dist_eq x z (div_nonneg hε.le $ add_nonneg hε.le hδ.le) (div_nonneg hδ.le $
+    add_nonneg hε.le hδ.le) $ by rw [←add_div, div_self (add_pos hε hδ).ne']).imp (λ y hy, _),
+  rw [hy.1, hy.2, div_mul_comm', div_mul_comm' ε],
+  rw ←div_lt_one (add_pos hε hδ) at h,
+  exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma disjoint_ball_ball_iff (hδ : 0 < δ) (hε : 0 < ε) :
+  disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y :=
+begin
+  refine ⟨λ h, le_of_not_lt $ λ hxy, _, ball_disjoint_ball⟩,
+  rw add_comm at hxy,
+  obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_lt hδ hε hxy,
+  rw dist_comm at hxz,
+  exact h ⟨hxz, hzy⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma disjoint_ball_closed_ball_iff (hδ : 0 < δ) (hε : 0 ≤ ε) :
+  disjoint (ball x δ) (closed_ball y ε) ↔ δ + ε ≤ dist x y :=
+begin
+  refine ⟨λ h, le_of_not_lt $ λ hxy, _, ball_disjoint_closed_ball⟩,
+  rw add_comm at hxy,
+  obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy,
+  rw dist_comm at hxz,
+  exact h ⟨hxz, hzy⟩,
+end
+
+-- This is also true for `ℚ`-normed spaces
+lemma disjoint_closed_ball_ball_iff (hδ : 0 ≤ δ) (hε : 0 < ε) :
+  disjoint (closed_ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y :=
+by rw [disjoint.comm, disjoint_ball_closed_ball_iff hε hδ, add_comm, dist_comm]; apply_instance
+
+lemma disjoint_closed_ball_closed_ball_iff (hδ : 0 ≤ δ) (hε : 0 ≤ ε) :
+  disjoint (closed_ball x δ) (closed_ball y ε) ↔ δ + ε < dist x y :=
+begin
+  refine ⟨λ h, lt_of_not_ge $ λ hxy, _, closed_ball_disjoint_closed_ball⟩,
+  rw add_comm at hxy,
+  obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy,
+  rw dist_comm at hxz,
+  exact h ⟨hxz, hzy⟩,
+end
+
 end semi_normed_group
 
 section normed_group

src/topology/metric_space/basic.lean

@@ -389,7 +389,7 @@ by rw [edist_dist, ennreal.to_real_of_real (dist_nonneg)]
 namespace metric
 
 /- instantiate pseudometric space as a topology -/
-variables {x y z : α} {ε ε₁ ε₂ : ℝ} {s : set α}
+variables {x y z : α} {δ ε ε₁ ε₂ : ℝ} {s : set α}
 
 /-- `ball x ε` is the set of all points `y` with `dist y x < ε` -/
 def ball (x : α) (ε : ℝ) : set α := {y | dist y x < ε}
@@ -466,31 +466,18 @@ assume y (hy : _ < _), le_of_lt hy
 theorem sphere_subset_closed_ball : sphere x ε ⊆ closed_ball x ε :=
 λ y, le_of_eq
 
-lemma closed_ball_disjoint_ball (x y : α) (rx ry : ℝ) (h : rx + ry ≤ dist x y) :
-  disjoint (closed_ball x rx) (ball y ry) :=
-begin
-  rw disjoint_left,
-  intros a ax ay,
-  apply lt_irrefl (dist x y),
-  calc dist x y ≤ dist a x + dist a y : dist_triangle_left _ _ _
-  ... < rx + ry : add_lt_add_of_le_of_lt (mem_closed_ball.1 ax) (mem_ball.1 ay)
-  ... ≤ dist x y : h
-end
+lemma closed_ball_disjoint_ball (h : δ + ε ≤ dist x y) : disjoint (closed_ball x δ) (ball y ε) :=
+λ a ha, (h.trans $ dist_triangle_left _ _ _).not_lt $ add_lt_add_of_le_of_lt ha.1 ha.2
 
-lemma ball_disjoint_ball (x y : α) (rx ry : ℝ) (h : rx + ry ≤ dist x y) :
-  disjoint (ball x rx) (ball y ry) :=
-(closed_ball_disjoint_ball x y rx ry h).mono_left ball_subset_closed_ball
+lemma ball_disjoint_closed_ball (h : δ + ε ≤ dist x y) : disjoint (ball x δ) (closed_ball y ε) :=
+(closed_ball_disjoint_ball $ by rwa [add_comm, dist_comm]).symm
 
-lemma closed_ball_disjoint_closed_ball {x y : α} {rx ry : ℝ} (h : rx + ry < dist x y) :
-  disjoint (closed_ball x rx) (closed_ball y ry) :=
-begin
-  rw disjoint_left,
-  intros a ax ay,
-  apply lt_irrefl (dist x y),
-  calc dist x y ≤ dist a x + dist a y : dist_triangle_left _ _ _
-  ... ≤ rx + ry : add_le_add ax ay
-  ... < dist x y : h
-end
+lemma ball_disjoint_ball (h : δ + ε ≤ dist x y) : disjoint (ball x δ) (ball y ε) :=
+(closed_ball_disjoint_ball h).mono_left ball_subset_closed_ball
+
+lemma closed_ball_disjoint_closed_ball (h : δ + ε < dist x y) :
+  disjoint (closed_ball x δ) (closed_ball y ε) :=
+λ a ha, h.not_le $ (dist_triangle_left _ _ _).trans $ add_le_add ha.1 ha.2
 
 theorem sphere_disjoint_ball : disjoint (sphere x ε) (ball x ε) :=
 λ y ⟨hy₁, hy₂⟩, absurd hy₁ $ ne_of_lt hy₂