chore(analysis): move lemmas around (#12621)

* move `smul_unit_ball` to `analysis.normed_space.pointwise`, rename it to `smul_unit_ball_of_pos`;
* reorder lemmas in `analysis.normed_space.pointwise`;
* add `vadd_ball_zero`, `vadd_closed_ball_zero`, `smul_unit`, `affinity_unit_ball`, `affinity_unit_closed_ball`.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/analysis/convex/gauge.lean

@@ -440,12 +440,9 @@ begin
     exact lt_irrefl _ h }
 end
 
-lemma smul_unit_ball {r : ℝ} (hr : 0 < r) : r • metric.ball (0 : E) 1 = metric.ball (0 : E) r :=
-by rw [smul_ball hr.ne', smul_zero, mul_one, real.norm_of_nonneg hr.le]
-
 lemma gauge_ball (hr : 0 < r) (x : E) : gauge (metric.ball (0 : E) r) x = ∥x∥ / r :=
 begin
-  rw [←smul_unit_ball hr, gauge_smul_left, pi.smul_apply, gauge_unit_ball, smul_eq_mul,
+  rw [←smul_unit_ball_of_pos hr, gauge_smul_left, pi.smul_apply, gauge_unit_ball, smul_eq_mul,
     abs_of_nonneg hr.le, div_eq_inv_mul],
   simp_rw [mem_ball_zero_iff, norm_neg],
   exact λ _, id,

src/analysis/normed_space/pointwise.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed.group.pointwise
+import analysis.normed.group.add_torsor
 import analysis.normed_space.basic
 import topology.metric_space.hausdorff_distance
 
@@ -18,9 +19,10 @@ multiplication of bounded sets remain bounded.
 open metric set
 open_locale pointwise topological_space
 
-section normed_space
+variables {𝕜 E : Type*} [normed_field 𝕜]
 
-variables {𝕜 : Type*} [normed_field 𝕜] {E : Type*} [semi_normed_group E] [normed_space 𝕜 E]
+section semi_normed_group
+variables [semi_normed_group E] [normed_space 𝕜 E]
 
 theorem smul_ball {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
   c • ball x r = ball (c • x) (∥c∥ * r) :=
@@ -31,6 +33,9 @@ begin
   simp [← div_eq_inv_mul, div_lt_iff (norm_pos_iff.2 hc), mul_comm _ r, dist_smul],
 end
 
+lemma smul_unit_ball {c : 𝕜} (hc : c ≠ 0) : c • ball (0 : E) (1 : ℝ) = ball (0 : E) (∥c∥) :=
+by rw [smul_ball hc, smul_zero, mul_one]
+
 theorem smul_sphere' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
   c • sphere x r = sphere (c • x) (∥c∥ * r) :=
 begin
@@ -41,28 +46,6 @@ begin
     div_eq_iff (norm_pos_iff.2 hc).ne', mul_comm r],
 end
 
-/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
-nonnegative. -/
-@[simp] theorem normed_space.sphere_nonempty {E : Type*} [normed_group E]
-  [normed_space ℝ E] [nontrivial E] {x : E} {r : ℝ} :
-  (sphere x r).nonempty ↔ 0 ≤ r :=
-begin
-  refine ⟨λ h, nonempty_closed_ball.1 (h.mono sphere_subset_closed_ball), λ hr, _⟩,
-  rcases exists_ne x with ⟨y, hy⟩,
-  have : ∥y - x∥ ≠ 0, by simpa [sub_eq_zero],
-  use r • ∥y - x∥⁻¹ • (y - x) + x,
-  simp [norm_smul, this, real.norm_of_nonneg hr]
-end
-
-theorem smul_sphere {E : Type*} [normed_group E] [normed_space 𝕜 E] [normed_space ℝ E]
-  [nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
-  c • sphere x r = sphere (c • x) (∥c∥ * r) :=
-begin
-  rcases eq_or_ne c 0 with rfl|hc,
-  { simp [zero_smul_set, set.singleton_zero, hr] },
-  { exact smul_sphere' hc x r }
-end
-
 theorem smul_closed_ball' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
   c • closed_ball x r = closed_ball (c • x) (∥c∥ * r) :=
 by simp only [← ball_union_sphere, set.smul_set_union, smul_ball hc, smul_sphere' hc]
@@ -122,11 +105,25 @@ begin
   rw [smul_smul, inv_mul_cancel hc, one_smul],
 end
 
-end normed_space
+/-- 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]
 
-section normed_space
+/-- 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 {𝕜 : Type*} [normed_field 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables [normed_space ℝ 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]
+
+end semi_normed_group
+
+section normed_group
+variables [normed_group E] [normed_space 𝕜 E]
 
 theorem smul_closed_ball (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
   c • closed_ball x r = closed_ball (c • x) (∥c∥ * r) :=
@@ -136,4 +133,45 @@ begin
   { exact smul_closed_ball' hc x r }
 end
 
-end normed_space
+lemma smul_closed_unit_ball (c : 𝕜) : c • closed_ball (0 : E) (1 : ℝ) = closed_ball (0 : E) (∥c∥) :=
+by rw [smul_closed_ball _ _ zero_le_one, smul_zero, mul_one]
+
+variables [normed_space ℝ E]
+
+/-- In a real normed space, the image of the unit closed ball under multiplication by a nonnegative
+number `r` is the closed ball of radius `r` with center at the origin. -/
+lemma smul_closed_unit_ball_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
+  r • closed_ball 0 1 = closed_ball (0 : E) r :=
+by rw [smul_closed_unit_ball, real.norm_of_nonneg hr]
+
+/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
+nonnegative. -/
+@[simp] lemma normed_space.sphere_nonempty [nontrivial E] {x : E} {r : ℝ} :
+  (sphere x r).nonempty ↔ 0 ≤ r :=
+begin
+  obtain ⟨y, hy⟩ := exists_ne x,
+  refine ⟨λ h, nonempty_closed_ball.1 (h.mono sphere_subset_closed_ball), λ hr,
+    ⟨r • ∥y - x∥⁻¹ • (y - x) + x, _⟩⟩,
+  have : ∥y - x∥ ≠ 0, by simpa [sub_eq_zero],
+  simp [norm_smul, this, real.norm_of_nonneg hr],
+end
+
+lemma smul_sphere [nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
+  c • sphere x r = sphere (c • x) (∥c∥ * r) :=
+begin
+  rcases eq_or_ne c 0 with rfl|hc,
+  { simp [zero_smul_set, set.singleton_zero, hr] },
+  { exact smul_sphere' hc x r }
+end
+
+/-- Any ball `metric.ball x r`, `0 < r` is the image of the unit ball under `λ y, x + r • y`. -/
+lemma affinity_unit_ball {r : ℝ} (hr : 0 < r) (x : E) : x +ᵥ r • ball 0 1 = ball x r :=
+by rw [smul_unit_ball_of_pos hr, vadd_ball_zero]
+
+/-- Any closed ball `metric.closed_ball x r`, `0 ≤ r` is the image of the unit closed ball under
+`λ y, x + r • y`. -/
+lemma affinity_unit_closed_ball {r : ℝ} (hr : 0 ≤ r) (x : E) :
+  x +ᵥ r • closed_ball 0 1 = closed_ball x r :=
+by rw [smul_closed_unit_ball, real.norm_of_nonneg hr, vadd_closed_ball_zero]
+
+end normed_group