From aa1dbeab548d61bc840a099abae4437046eaaf00 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 4 May 2023 03:36:49 +0000
Subject: [PATCH] chore(analysis/normed_space/extend): golf, add aux lemmas
 (#18927)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Add `linear_map.extend_to_𝕜'_apply_re`,
  `linear_map.sq_norm_extend_to_𝕜'_apply`,
  `continuous_linear_map.norm_extend_to_𝕜`, and
  `continuous_linear_map.norm_extend_to_𝕜'`.
* Rename `norm_bound` to
  `continuous_linear_map.norm_extend_to_𝕜'_bound`.
* Golf, use `namespace`s.
---
 src/analysis/normed_space/extend.lean         | 89 ++++++++++---------
 .../normed_space/hahn_banach/extension.lean   |  2 +-
 2 files changed, 47 insertions(+), 44 deletions(-)

diff --git a/src/analysis/normed_space/extend.lean b/src/analysis/normed_space/extend.lean
index f0a198fc8ed45..bc01ce94c0d2b 100644
--- a/src/analysis/normed_space/extend.lean
+++ b/src/analysis/normed_space/extend.lean
@@ -32,14 +32,17 @@ Alternate forms which operate on `[is_scalar_tower ℝ 𝕜 F]` instead are prov
 -/
 
 open is_R_or_C
+open_locale complex_conjugate
 
 variables {𝕜 : Type*} [is_R_or_C 𝕜] {F : Type*} [seminormed_add_comm_group F] [normed_space 𝕜 F]
-local notation `abs𝕜` := @is_R_or_C.abs 𝕜 _
+
+namespace linear_map
+
+variables [module ℝ F] [is_scalar_tower ℝ 𝕜 F]
 
 /-- Extend `fr : F →ₗ[ℝ] ℝ` to `F →ₗ[𝕜] 𝕜` in a way that will also be continuous and have its norm
 bounded by `‖fr‖` if `fr` is continuous. -/
-noncomputable def linear_map.extend_to_𝕜'
-  [module ℝ F] [is_scalar_tower ℝ 𝕜 F] (fr : F →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜 :=
+noncomputable def extend_to_𝕜' (fr : F →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜 :=
 begin
   let fc : F → 𝕜 := λ x, (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x)),
   have add : ∀ x y : F, fc (x + y) = fc x + fc y,
@@ -73,61 +76,57 @@ begin
   exact { to_fun := fc, map_add' := add, map_smul' := smul_𝕜 }
 end
 
-lemma linear_map.extend_to_𝕜'_apply [module ℝ F] [is_scalar_tower ℝ 𝕜 F]
-  (fr : F →ₗ[ℝ] ℝ) (x : F) :
+lemma extend_to_𝕜'_apply (fr : F →ₗ[ℝ] ℝ) (x : F) :
   fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
 
+@[simp] lemma extend_to_𝕜'_apply_re (fr : F →ₗ[ℝ] ℝ) (x : F) : re (fr.extend_to_𝕜' x : 𝕜) = fr x :=
+by simp only [extend_to_𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero] with is_R_or_C_simps
+
+lemma norm_extend_to_𝕜'_apply_sq (f : F →ₗ[ℝ] ℝ) (x : F) :
+  ‖(f.extend_to_𝕜' x : 𝕜)‖ ^ 2 = f (conj (f.extend_to_𝕜' x : 𝕜) • x) :=
+calc ‖(f.extend_to_𝕜' x : 𝕜)‖ ^ 2 = re (conj (f.extend_to_𝕜' x) * f.extend_to_𝕜' x : 𝕜) :
+  by rw [is_R_or_C.conj_mul_eq_norm_sq_left, norm_sq_eq_def', of_real_re]
+... = f (conj (f.extend_to_𝕜' x : 𝕜) • x) :
+  by rw [← smul_eq_mul, ← map_smul, extend_to_𝕜'_apply_re]
+
+end linear_map
+
+namespace continuous_linear_map
+
+variables [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
+
 /-- The norm of the extension is bounded by `‖fr‖`. -/
-lemma norm_bound [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) :
+lemma norm_extend_to_𝕜'_bound (fr : F →L[ℝ] ℝ) (x : F) :
   ‖(fr.to_linear_map.extend_to_𝕜' x : 𝕜)‖ ≤ ‖fr‖ * ‖x‖ :=
 begin
-  let lm : F →ₗ[𝕜] 𝕜 := fr.to_linear_map.extend_to_𝕜',
-  -- We aim to find a `t : 𝕜` such that
-  -- * `lm (t • x) = fr (t • x)` (so `lm (t • x) = t * lm x ∈ ℝ`)
-  -- * `‖lm x‖ = ‖lm (t • x)‖` (so `t.abs` must be 1)
-  -- If `lm x ≠ 0`, `(lm x)⁻¹` satisfies the first requirement, and after normalizing, it
-  -- satisfies the second.
-  -- (If `lm x = 0`, the goal is trivial.)
+  set lm : F →ₗ[𝕜] 𝕜 := fr.to_linear_map.extend_to_𝕜',
   classical,
   by_cases h : lm x = 0,
   { rw [h, norm_zero],
     apply mul_nonneg; exact norm_nonneg _ },
-  let fx := (lm x)⁻¹,
-  let t := fx / (abs𝕜 fx : 𝕜),
-  have ht : abs𝕜 t = 1, by field_simp [abs_of_real, of_real_inv, is_R_or_C.abs_inv,
-    is_R_or_C.abs_div, is_R_or_C.abs_abs, h],
-  have h1 : (fr (t • x) : 𝕜) = lm (t • x),
-  { apply ext,
-    { simp only [lm, of_real_re, linear_map.extend_to_𝕜'_apply, mul_re, I_re, of_real_im, zero_mul,
-        add_monoid_hom.map_sub, sub_zero, mul_zero],
-      refl },
-    { symmetry,
-      calc im (lm (t • x))
-          = im (t * lm x) : by rw [lm.map_smul, smul_eq_mul]
-      ... = im ((lm x)⁻¹ / (abs𝕜 (lm x)⁻¹) * lm x) : rfl
-      ... = im (1 / (abs𝕜 (lm x)⁻¹ : 𝕜)) : by rw [div_mul_eq_mul_div, inv_mul_cancel h]
-      ... = 0 : by rw [← of_real_one, ← of_real_div, of_real_im]
-      ... = im (fr (t • x) : 𝕜) : by rw [of_real_im] } },
-  calc ‖lm x‖ = abs𝕜 t * ‖lm x‖ : by rw [ht, one_mul]
-  ... = ‖t * lm x‖ : by rw [← norm_eq_abs, norm_mul]
-  ... = ‖lm (t • x)‖ : by rw [←smul_eq_mul, lm.map_smul]
-  ... = ‖(fr (t • x) : 𝕜)‖ : by rw h1
-  ... = ‖fr (t • x)‖ : by rw [norm_eq_abs, abs_of_real, norm_eq_abs, abs_to_real]
-  ... ≤ ‖fr‖ * ‖t • x‖ : continuous_linear_map.le_op_norm _ _
-  ... = ‖fr‖ * (‖t‖ * ‖x‖) : by rw norm_smul
-  ... ≤ ‖fr‖ * ‖x‖ : by rw [norm_eq_abs, ht, one_mul]
+  rw [← mul_le_mul_left (norm_pos_iff.2 h), ← sq],
+  calc ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) : fr.to_linear_map.norm_extend_to_𝕜'_apply_sq x
+  ... ≤ ‖fr (conj (lm x : 𝕜) • x)‖ : le_abs_self _
+  ... ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ : le_op_norm _ _
+  ... = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) : by rw [norm_smul, norm_conj, mul_left_comm]
 end
 
 /-- Extend `fr : F →L[ℝ] ℝ` to `F →L[𝕜] 𝕜`. -/
-noncomputable def continuous_linear_map.extend_to_𝕜' [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
-  (fr : F →L[ℝ] ℝ) :
-  F →L[𝕜] 𝕜 :=
-linear_map.mk_continuous _ (‖fr‖) (norm_bound _)
+noncomputable def extend_to_𝕜' (fr : F →L[ℝ] ℝ) : F →L[𝕜] 𝕜 :=
+linear_map.mk_continuous _ (‖fr‖) fr.norm_extend_to_𝕜'_bound
 
-lemma continuous_linear_map.extend_to_𝕜'_apply [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
-  (fr : F →L[ℝ] ℝ) (x : F) :
+lemma extend_to_𝕜'_apply (fr : F →L[ℝ] ℝ) (x : F) :
   fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
 
+@[simp] lemma norm_extend_to_𝕜' (fr : F →L[ℝ] ℝ) : ‖(fr.extend_to_𝕜' : F →L[𝕜] 𝕜)‖ = ‖fr‖ :=
+le_antisymm (linear_map.mk_continuous_norm_le _ (norm_nonneg _) _) $
+  op_norm_le_bound _ (norm_nonneg _) $ λ x,
+    calc ‖fr x‖ = ‖re (fr.extend_to_𝕜' x : 𝕜)‖ : congr_arg norm (fr.extend_to_𝕜'_apply_re x).symm
+    ... ≤ ‖(fr.extend_to_𝕜' x : 𝕜)‖ : (abs_re_le_abs _).trans_eq (norm_eq_abs _).symm
+    ... ≤ ‖(fr.extend_to_𝕜' : F →L[𝕜] 𝕜)‖ * ‖x‖ : le_op_norm _ _
+
+end continuous_linear_map
+
 /-- Extend `fr : restrict_scalars ℝ 𝕜 F →ₗ[ℝ] ℝ` to `F →ₗ[𝕜] 𝕜`. -/
 noncomputable def linear_map.extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜 :=
 fr.extend_to_𝕜'
@@ -142,3 +141,7 @@ fr.extend_to_𝕜'
 
 lemma continuous_linear_map.extend_to_𝕜_apply (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) (x : F) :
   fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x : _) := rfl
+
+@[simp] lemma continuous_linear_map.norm_extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) :
+  ‖fr.extend_to_𝕜‖ = ‖fr‖ :=
+fr.norm_extend_to_𝕜'
diff --git a/src/analysis/normed_space/hahn_banach/extension.lean b/src/analysis/normed_space/hahn_banach/extension.lean
index 74898d0c531ca..80ab1610e970d 100644
--- a/src/analysis/normed_space/hahn_banach/extension.lean
+++ b/src/analysis/normed_space/hahn_banach/extension.lean
@@ -92,7 +92,7 @@ begin
   -- And we derive the equality of the norms by bounding on both sides.
   refine ⟨h, le_antisymm _ _⟩,
   { calc ‖g.extend_to_𝕜‖
-        ≤ ‖g‖ : g.extend_to_𝕜.op_norm_le_bound g.op_norm_nonneg (norm_bound _)
+        = ‖g‖ : g.norm_extend_to_𝕜
     ... = ‖fr‖ : hnormeq
     ... ≤ ‖re_clm‖ * ‖f‖ : continuous_linear_map.op_norm_comp_le _ _
     ... = ‖f‖ : by rw [re_clm_norm, one_mul] },