feat(analysis/normed_space/basic): the rescaling of a ball is a ball (#…

…9297)

Also rename all statements with `ball_0` to `ball_zero` for coherence.

src/algebra/pointwise.lean

@@ -622,6 +622,9 @@ by simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]
 lemma preimage_smul (a : α) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
 ((mul_action.to_perm a).symm.image_eq_preimage _).symm
 
+lemma preimage_smul_inv (a : α) (t : set β) : (λ x, a⁻¹ • x) ⁻¹' t = a • t :=
+preimage_smul (to_units a)⁻¹ t
+
 @[simp] lemma set_smul_subset_set_smul_iff {a : α} {A B : set β} : a • A ⊆ a • B ↔ A ⊆ B :=
 image_subset_image_iff $ mul_action.injective _
 
@@ -652,6 +655,10 @@ show _ ∈ (units.mk0 a ha)⁻¹ • _ ↔ _, from mem_inv_smul_set_iff
 lemma preimage_smul' {a : α} (ha : a ≠ 0) (t : set β) : (λ x, a • x) ⁻¹' t = a⁻¹ • t :=
 preimage_smul (units.mk0 a ha) t
 
+lemma preimage_smul_inv' {a : α} (ha : a ≠ 0) (t : set β) :
+  (λ x, a⁻¹ • x) ⁻¹' t = a • t :=
+preimage_smul ((units.mk0 a ha)⁻¹) t
+
 @[simp] lemma set_smul_subset_set_smul_iff' {a : α} (ha : a ≠ 0) {A B : set β} :
   a • A ⊆ a • B ↔ A ⊆ B :=
 show units.mk0 a ha • _ ⊆ _ ↔ _, from set_smul_subset_set_smul_iff

src/analysis/analytic/basic.lean

@@ -217,7 +217,7 @@ lemma summable_norm_apply (p : formal_multilinear_series 𝕜 E F)
   {x : E} (hx : x ∈ emetric.ball (0 : E) p.radius) :
   summable (λ n : ℕ, ∥p n (λ _, x)∥) :=
 begin
-  rw mem_emetric_ball_0_iff at hx,
+  rw mem_emetric_ball_zero_iff at hx,
   refine summable_of_nonneg_of_le (λ _, norm_nonneg _) (λ n, ((p n).le_op_norm _).trans_eq _)
     (p.summable_norm_mul_pow hx),
   simp
@@ -438,10 +438,10 @@ begin
   obtain ⟨a, ha, C, hC, hp⟩ : ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), ∀ n, ∥p n∥ * r' ^n ≤ C * a^n :=
     p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le),
   refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), λ y hy n, _⟩,
-  have yr' : ∥y∥ < r', by { rw ball_0_eq at hy, exact hy },
+  have yr' : ∥y∥ < r', by { rw ball_zero_eq at hy, exact hy },
   have hr'0 : 0 < (r' : ℝ), from (norm_nonneg _).trans_lt yr',
   have : y ∈ emetric.ball (0 : E) r,
-  { refine mem_emetric_ball_0_iff.2 (lt_trans _ h),
+  { refine mem_emetric_ball_zero_iff.2 (lt_trans _ h),
     exact_mod_cast yr' },
   rw [norm_sub_rev, ← mul_div_right_comm],
   have ya : a * (∥y∥ / ↑r') ≤ a,
@@ -471,7 +471,7 @@ begin
     (∀ y ∈ metric.ball (0 : E) r', ∀ n, ∥f (x + y) - p.partial_sum n y∥ ≤ C * (a * (∥y∥ / r')) ^ n),
     from hf.uniform_geometric_approx' h,
   refine ⟨a, ha, C, hC, λ y hy n, (hp y hy n).trans _⟩,
-  have yr' : ∥y∥ < r', by rwa ball_0_eq at hy,
+  have yr' : ∥y∥ < r', by rwa ball_zero_eq at hy,
   refine mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left _ _ _) hC.lt.le,
   exacts [mul_nonneg ha.1.le (div_nonneg (norm_nonneg y) r'.coe_nonneg),
     mul_le_of_le_one_right ha.1.le (div_le_one_of_le yr'.le r'.coe_nonneg)]
@@ -893,12 +893,12 @@ theorem change_origin_eval (h : (∥x∥₊ + ∥y∥₊ : ℝ≥0∞) < p.radiu
 begin
   have radius_pos : 0 < p.radius := lt_of_le_of_lt (zero_le _) h,
   have x_mem_ball : x ∈ emetric.ball (0 : E) p.radius,
-    from mem_emetric_ball_0_iff.2 ((le_add_right le_rfl).trans_lt h),
+    from mem_emetric_ball_zero_iff.2 ((le_add_right le_rfl).trans_lt h),
   have y_mem_ball : y ∈ emetric.ball (0 : E) (p.change_origin x).radius,
-  { refine mem_emetric_ball_0_iff.2 (lt_of_lt_of_le _ p.change_origin_radius),
+  { refine mem_emetric_ball_zero_iff.2 (lt_of_lt_of_le _ p.change_origin_radius),
     rwa [ennreal.lt_sub_iff_add_lt, add_comm] },
   have x_add_y_mem_ball : x + y ∈ emetric.ball (0 : E) p.radius,
-  { refine mem_emetric_ball_0_iff.2 (lt_of_le_of_lt _ h),
+  { refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt _ h),
     exact_mod_cast nnnorm_add_le x y },
   set f : (Σ (k l : ℕ), {s : finset (fin (k + l)) // s.card = l}) → F :=
     λ s, p.change_origin_series_term s.1 s.2.1 s.2.2 s.2.2.2 (λ _, x) (λ _, y),
@@ -916,7 +916,7 @@ begin
       { simp only [change_origin_series, continuous_multilinear_map.sum_apply],
         apply has_sum_fintype },
       { refine summable_of_nnnorm_bounded _ (p.change_origin_series_summable_aux₂
-          (mem_emetric_ball_0_iff.1 x_mem_ball) k) (λ s, _),
+          (mem_emetric_ball_zero_iff.1 x_mem_ball) k) (λ s, _),
         refine (continuous_multilinear_map.le_op_nnnorm _ _).trans_eq _,
         simp } } },
   refine hf.unique (change_origin_index_equiv.symm.has_sum_iff.1 _),
@@ -954,9 +954,9 @@ theorem has_fpower_series_on_ball.change_origin
   r_pos := by simp [h],
   has_sum := λ z hz, begin
     convert (p.change_origin y).has_sum _,
-    { rw [mem_emetric_ball_0_iff, ennreal.lt_sub_iff_add_lt, add_comm] at hz,
+    { rw [mem_emetric_ball_zero_iff, ennreal.lt_sub_iff_add_lt, add_comm] at hz,
       rw [p.change_origin_eval (hz.trans_le hf.r_le), add_assoc, hf.sum],
-      refine mem_emetric_ball_0_iff.2 (lt_of_le_of_lt _ hz),
+      refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt _ hz),
       exact_mod_cast nnnorm_add_le y z },
     { refine emetric.ball_subset_ball (le_trans _ p.change_origin_radius) hz,
       exact ennreal.sub_le_sub hf.r_le le_rfl }

src/analysis/normed_space/basic.lean

@@ -25,7 +25,7 @@ variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
 noncomputable theory
 open filter metric
-open_locale topological_space big_operators nnreal ennreal uniformity
+open_locale topological_space big_operators nnreal ennreal uniformity pointwise
 
 /-- Auxiliary class, endowing a type `α` with a function `norm : α → ℝ`. This class is designed to
 be extended in more interesting classes specifying the properties of the norm. -/
@@ -227,7 +227,7 @@ calc ∥v∥ = ∥u - (u - v)∥ : by abel
 lemma norm_le_insert' (u v : α) : ∥u∥ ≤ ∥v∥ + ∥u - v∥ :=
 by { rw norm_sub_rev, exact norm_le_insert v u }
 
-lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
+lemma ball_zero_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
 lemma mem_ball_iff_norm {g h : α} {r : ℝ} :
@@ -242,7 +242,7 @@ lemma mem_ball_iff_norm' {g h : α} {r : ℝ} :
   h ∈ ball g r ↔ ∥g - h∥ < r :=
 by rw [mem_ball', dist_eq_norm]
 
-@[simp] lemma mem_ball_0_iff {ε : ℝ} {x : α} : x ∈ ball (0 : α) ε ↔ ∥x∥ < ε :=
+@[simp] lemma mem_ball_zero_iff {ε : ℝ} {x : α} : x ∈ ball (0 : α) ε ↔ ∥x∥ < ε :=
 by rw [mem_ball, dist_zero_right]
 
 lemma mem_closed_ball_iff_norm {g h : α} {r : ℝ} :
@@ -285,6 +285,21 @@ begin
   exact exists_congr (λ r, by simp [(⊆), set.subset]),
 end
 
+lemma preimage_add_ball (x y : α) (r : ℝ) : ((+) y) ⁻¹' (ball x r) = ball (x - y) r :=
+begin
+  ext z,
+  simp only [dist_eq_norm, set.mem_preimage, mem_ball],
+  abel
+end
+
+lemma preimage_add_closed_ball (x y : α) (r : ℝ) :
+  ((+) y) ⁻¹' (closed_ball x r) = closed_ball (x - y) r :=
+begin
+  ext z,
+  simp only [dist_eq_norm, set.mem_preimage, mem_closed_ball],
+  abel
+end
+
 @[simp] lemma mem_sphere_iff_norm (v w : α) (r : ℝ) : w ∈ sphere v r ↔ ∥w - v∥ = r :=
 by simp [dist_eq_norm]
 
@@ -294,6 +309,14 @@ by simp [dist_eq_norm]
 @[simp] lemma norm_eq_of_mem_sphere {r : ℝ} (x : sphere (0:α) r) : ∥(x:α)∥ = r :=
 mem_sphere_zero_iff_norm.mp x.2
 
+lemma preimage_add_sphere (x y : α) (r : ℝ) :
+  ((+) y) ⁻¹' (sphere x r) = sphere (x - y) r :=
+begin
+  ext z,
+  simp only [set.mem_preimage, mem_sphere_iff_norm],
+  abel
+end
+
 lemma ne_zero_of_norm_pos {g : α} : 0 < ∥ g ∥ → g ≠ 0 :=
 begin
   intros hpos hzero,
@@ -547,7 +570,7 @@ by rw [edist_dist, dist_eq_norm, of_real_norm_eq_coe_nnnorm]
 lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (∥x∥₊ : ℝ≥0∞) :=
 by rw [edist_eq_coe_nnnorm_sub, _root_.sub_zero]
 
-lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥x∥₊ < r :=
+lemma mem_emetric_ball_zero_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥x∥₊ < r :=
 by rw [emetric.mem_ball, edist_eq_coe_nnnorm]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : α) :
@@ -1607,6 +1630,33 @@ theorem frontier_closed_ball [semi_normed_space ℝ E] (x : E) {r : ℝ} (hr : 0
 by rw [frontier, closure_closed_ball, interior_closed_ball x hr,
   closed_ball_diff_ball]
 
+theorem smul_ball {c : α} (hc : c ≠ 0) (x : E) (r : ℝ) :
+  c • ball x r = ball (c • x) (∥c∥ * r) :=
+begin
+  ext y,
+  rw mem_smul_set_iff_inv_smul_mem' hc,
+  conv_lhs { rw ←inv_smul_smul' hc x },
+  simp [← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hc), mul_comm _ r, dist_smul],
+end
+
+theorem smul_closed_ball' {c : α} (hc : c ≠ 0) (x : E) (r : ℝ) :
+  c • closed_ball x r = closed_ball (c • x) (∥c∥ * r) :=
+begin
+  ext y,
+  rw mem_smul_set_iff_inv_smul_mem' hc,
+  conv_lhs { rw ←inv_smul_smul' hc x },
+  simp [dist_smul, ← div_eq_inv_mul, div_le_iff (norm_pos_iff.2 hc), mul_comm _ r],
+end
+
+theorem smul_closed_ball {E : Type*} [normed_group E] [normed_space α E]
+  (c : α) (x : E) {r : ℝ} (hr : 0 ≤ r) :
+  c • closed_ball x r = closed_ball (c • x) (∥c∥ * r) :=
+begin
+  rcases eq_or_ne c 0 with rfl|hc,
+  { simp [hr, zero_smul_set, set.singleton_zero, ← nonempty_closed_ball] },
+  { exact smul_closed_ball' hc x r }
+end
+
 variables (α)
 
 lemma ne_neg_of_mem_sphere [char_zero α] {r : ℝ} (hr : 0 < r) (x : sphere (0:E) r) : x ≠ - x :=
@@ -1877,7 +1927,7 @@ lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → α} :
     ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
 begin
   rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff],
-  { simp only [ball_0_eq, set.mem_set_of_eq] },
+  { simp only [ball_zero_eq, set.mem_set_of_eq] },
   { rintros s t hst ⟨s', hs'⟩,
     exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ }
 end

src/analysis/normed_space/normed_group_quotient.lean

@@ -258,13 +258,13 @@ lemma quotient_nhd_basis (S : add_subgroup M) :
     dsimp at x_in,
     rcases norm_mk_lt x (half_pos ε_pos) with ⟨y, rfl, ry⟩,
     apply H,
-    rw ball_0_eq,
+    rw ball_zero_eq,
     dsimp,
     linarith },
   { rintros ⟨ε, ε_pos, h⟩,
     have : (mk' S) '' (ball (0 : M) ε) ⊆ {x | ∥x∥ < ε},
     { rintros - ⟨x, x_in, rfl⟩,
-      rw mem_ball_0_iff at x_in,
+      rw mem_ball_zero_iff at x_in,
       exact lt_of_le_of_lt (quotient_norm_mk_le S x) x_in },
     apply filter.mem_of_superset _ (set.subset.trans this h),
     clear h U this,

src/analysis/normed_space/operator_norm.lean

@@ -274,7 +274,7 @@ lemma op_norm_le_of_ball {f : E →L[𝕜] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 <
 begin
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
   refine op_norm_le_of_shell ε_pos hC hc (λ x _ hx, hf x _),
-  rwa ball_0_eq
+  rwa ball_zero_eq
 end
 
 lemma op_norm_le_of_nhds_zero {f : E →L[𝕜] F} {C : ℝ} (hC : 0 ≤ C)
@@ -288,7 +288,7 @@ begin
   by_cases h0 : c = 0,
   { refine op_norm_le_of_ball ε_pos hC (λ x hx, hf x _ _),
     { simp [h0] },
-    { rwa ball_0_eq at hx } },
+    { rwa ball_zero_eq at hx } },
   { rw [← inv_inv' c, normed_field.norm_inv,
       inv_lt_one_iff_of_pos (norm_pos_iff.2 $ inv_ne_zero h0)] at hc,
     refine op_norm_le_of_shell ε_pos hC hc _,

src/topology/metric_space/basic.lean

@@ -378,6 +378,17 @@ assume y (hy : _ < _), le_of_lt hy
 theorem sphere_subset_closed_ball : sphere x ε ⊆ closed_ball x ε :=
 λ y, le_of_eq
 
+lemma ball_disjoint_ball (x y : α) (rx ry : ℝ) (h : rx + ry ≤ dist x y) :
+  disjoint (ball x rx) (ball y ry) :=
+begin
+  rw disjoint_left,
+  assume a ax ay,
+  apply lt_irrefl (dist x y),
+  calc dist x y ≤ dist x a + dist a y : dist_triangle _ _ _
+  ... < rx + ry : add_lt_add (mem_ball'.1 ax) (mem_ball.1 ay)
+  ... ≤ dist x y : h
+end
+
 theorem sphere_disjoint_ball : disjoint (sphere x ε) (ball x ε) :=
 λ y ⟨hy₁, hy₂⟩, absurd hy₁ $ ne_of_lt hy₂