From a3f4a025d4a736c57caa934467a5938beeda753a Mon Sep 17 00:00:00 2001
From: kkytola <kalle.kytola@aalto.fi>
Date: Wed, 27 Oct 2021 15:13:50 +0000
Subject: [PATCH] chore(analysis/normed_space/is_R_or_C +
 data/complex/is_R_or_C): make some proof steps standalone lemmas (#9933)

Separate some proof steps from `linear_map.bound_of_sphere_bound` as standalone lemmas to golf them a little bit.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
---
 src/analysis/normed_space/is_R_or_C.lean | 21 ++++++++-------------
 src/data/complex/is_R_or_C.lean          |  3 +++
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/analysis/normed_space/is_R_or_C.lean b/src/analysis/normed_space/is_R_or_C.lean
index 5c2b62a7e3d79..8bb5398339dde 100644
--- a/src/analysis/normed_space/is_R_or_C.lean
+++ b/src/analysis/normed_space/is_R_or_C.lean
@@ -27,27 +27,24 @@ 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 ∥ :=
+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 linear_map.bound_of_sphere_bound
-  {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
   {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], },
-  have norm_z_eq : ∥(∥ z ∥ : 𝕜)∥ =  ∥ z ∥,
-  { unfold_coes,
-    simp only [norm_algebra_map_eq, ring_hom.to_fun_eq_coe, norm_norm], },
-  have norm_r_eq : ∥(r : 𝕜)∥ = r,
-  { rw [is_R_or_C.norm_eq_abs, is_R_or_C.abs_of_real],
-    exact abs_of_pos r_pos, },
   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],
-    rw [norm_z_eq, mul_assoc, inv_mul_cancel (norm_pos_iff.mpr z_zero).ne.symm, mul_one],
+    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, },
@@ -56,15 +53,14 @@ begin
   { 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], },
-  rw [eq, normed_field.norm_mul, normed_field.norm_div, norm_z_eq, norm_r_eq,
-      div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm],
+  rw [eq, normed_field.norm_mul, normed_field.norm_div, is_R_or_C.norm_coe_norm,
+      is_R_or_C.norm_of_nonneg r_pos.le, div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm],
   apply div_le_div _ _ r_pos rfl.ge,
   { exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z), },
   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
-  {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
   {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 ∥ :=
@@ -74,7 +70,6 @@ begin
 end
 
 lemma continuous_linear_map.op_norm_bound_of_ball_bound
-  {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
   {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →L[𝕜] 𝕜)
   (h : ∀ z ∈ closed_ball (0 : E) r, ∥ f z ∥ ≤ c) : ∥ f ∥ ≤ c / r :=
 begin
diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean
index 462281fa82034..62ae83db7c497 100644
--- a/src/data/complex/is_R_or_C.lean
+++ b/src/data/complex/is_R_or_C.lean
@@ -429,6 +429,9 @@ by { rw [is_R_or_C.norm_eq_abs, is_R_or_C.abs_of_real, real.norm_eq_abs] }
 lemma abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : absK r = r :=
 (abs_of_real _).trans (abs_of_nonneg h)
 
+lemma norm_of_nonneg {r : ℝ} (r_nn : 0 ≤ r) : ∥(r : K)∥ = r :=
+by { rw norm_of_real, exact abs_eq_self.mpr r_nn, }
+
 lemma abs_of_nat (n : ℕ) : absK n = n :=
 by { rw [← of_real_nat_cast], exact abs_of_nonneg (nat.cast_nonneg n) }