feat(*/is_R_or_C): deduplicate (#10522)

I noticed that the same argument, that in a normed space over `is_R_or_C` an element can be normalized, appears in a couple of different places in the library.  I have deduplicated and placed it in `analysis/normed_space/is_R_or_C`.

src/analysis/inner_product_space/projection.lean

@@ -3,8 +3,9 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Frédéric Dupuis, Heather Macbeth
 -/
-import analysis.inner_product_space.basic
 import analysis.convex.basic
+import analysis.inner_product_space.basic
+import analysis.normed_space.is_R_or_C
 
 /-!
 # The orthogonal projection

src/analysis/normed_space/is_R_or_C.lean

@@ -28,28 +28,39 @@ This file exists mainly to avoid importing `is_R_or_C` in the main normed space
 open metric
 
 @[simp] lemma is_R_or_C.norm_coe_norm {𝕜 : Type*} [is_R_or_C 𝕜]
-  {E : Type*} [normed_group E] {z : E} : ∥(∥ z ∥ : 𝕜)∥ = ∥ z ∥ :=
+  {E : Type*} [normed_group E] {z : E} : ∥(∥z∥ : 𝕜)∥ = ∥z∥ :=
 by { unfold_coes, simp only [norm_algebra_map_eq, ring_hom.to_fun_eq_coe, norm_norm], }
 
 variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
 
+/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to unit length. -/
+@[simp] lemma norm_smul_inv_norm {x : E} (hx : x ≠ 0) : ∥(∥x∥⁻¹ : 𝕜) • x∥ = 1 :=
+begin
+  have : ∥x∥ ≠ 0 := by simp [hx],
+  field_simp [norm_smul]
+end
+
+/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to length `r`. -/
+lemma norm_smul_inv_norm' {r : ℝ} (r_nonneg : 0 ≤ r) {x : E} (hx : x ≠ 0) :
+  ∥(r * ∥x∥⁻¹ : 𝕜) • x∥ = r :=
+begin
+  have : ∥x∥ ≠ 0 := by simp [hx],
+  field_simp [norm_smul, is_R_or_C.norm_of_real, is_R_or_C.norm_eq_abs, r_nonneg]
+end
+
 lemma linear_map.bound_of_sphere_bound
-  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
-  (h : ∀ z ∈ sphere (0 : E) r, ∥ f z ∥ ≤ c) (z : E) : ∥ f z ∥ ≤ c / r * ∥ z ∥ :=
+  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ sphere (0 : E) r, ∥f z∥ ≤ c) (z : E) :
+  ∥f z∥ ≤ c / r * ∥z∥ :=
 begin
   by_cases z_zero : z = 0,
   { rw z_zero, simp only [linear_map.map_zero, norm_zero, mul_zero], },
-  set z₁ := (r * ∥ z ∥⁻¹ : 𝕜) • z with hz₁,
-  have norm_f_z₁ : ∥ f z₁ ∥ ≤ c,
-  { apply h z₁,
-    rw [mem_sphere_zero_iff_norm, hz₁, norm_smul, normed_field.norm_mul],
-    simp only [normed_field.norm_inv, is_R_or_C.norm_coe_norm],
-    rw [mul_assoc, inv_mul_cancel (norm_pos_iff.mpr z_zero).ne.symm, mul_one],
-    unfold_coes,
-    simp only [norm_algebra_map_eq, ring_hom.to_fun_eq_coe],
-    exact abs_of_pos r_pos, },
+  set z₁ := (r * ∥z∥⁻¹ : 𝕜) • z with hz₁,
+  have norm_f_z₁ : ∥f z₁∥ ≤ c,
+  { apply h,
+    rw mem_sphere_zero_iff_norm,
+    exact norm_smul_inv_norm' r_pos.le z_zero },
   have r_ne_zero : (r : 𝕜) ≠ 0 := (algebra_map ℝ 𝕜).map_ne_zero.mpr r_pos.ne.symm,
-  have eq : f z = ∥ z ∥ / r * (f z₁),
+  have eq : f z = ∥z∥ / r * (f z₁),
   { rw [hz₁, linear_map.map_smul, smul_eq_mul],
     rw [← mul_assoc, ← mul_assoc, div_mul_cancel _ r_ne_zero, mul_inv_cancel, one_mul],
     simp only [z_zero, is_R_or_C.of_real_eq_zero, norm_eq_zero, ne.def, not_false_iff], },
@@ -60,18 +71,14 @@ begin
   apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁),
 end
 
-lemma linear_map.bound_of_ball_bound
-  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
-  (h : ∀ z ∈ closed_ball (0 : E) r, ∥ f z ∥ ≤ c) :
-  ∀ (z : E), ∥ f z ∥ ≤ c / r * ∥ z ∥ :=
-begin
-  apply linear_map.bound_of_sphere_bound r_pos c f,
-  exact λ z hz, h z hz.le,
-end
+lemma linear_map.bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜)
+  (h : ∀ z ∈ closed_ball (0 : E) r, ∥f z∥ ≤ c) (z : E) :
+  ∥f z∥ ≤ c / r * ∥z∥ :=
+f.bound_of_sphere_bound r_pos c (λ z hz, h z hz.le) z
 
 lemma continuous_linear_map.op_norm_bound_of_ball_bound
-  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →L[𝕜] 𝕜)
-  (h : ∀ z ∈ closed_ball (0 : E) r, ∥ f z ∥ ≤ c) : ∥ f ∥ ≤ c / r :=
+  {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →L[𝕜] 𝕜) (h : ∀ z ∈ closed_ball (0 : E) r, ∥f z∥ ≤ c) :
+  ∥f∥ ≤ c / r :=
 begin
   apply continuous_linear_map.op_norm_le_bound,
   { apply div_nonneg _ r_pos.le,

src/data/complex/is_R_or_C.lean

@@ -786,24 +786,3 @@ linear_isometry.norm_to_continuous_linear_map of_real_li
 end linear_maps
 
 end is_R_or_C
-
-section normalization
-variables {K : Type*} [is_R_or_C K]
-variables {E : Type*} [normed_group E] [normed_space K E]
-
-open is_R_or_C
-
-/- Note: one might think the following lemma belongs in `analysis.normed_space.basic`.  But it
-can't be placed there, because that file is an import of `data.complex.is_R_or_C`! -/
-
-/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to unit length. -/
-@[simp] lemma norm_smul_inv_norm {x : E} (hx : x ≠ 0) : ∥(∥x∥⁻¹ : K) • x∥ = 1 :=
-begin
-  have h : ∥(∥x∥ : K)∥ = ∥x∥,
-  { rw norm_eq_abs,
-    exact abs_of_nonneg (norm_nonneg _) },
-  have : ∥x∥ ≠ 0 := by simp [hx],
-  field_simp [norm_smul, h]
-end
-
-end normalization