chore(analysis/normed_space/extend): provide a version without restrict_scalars (#6693)

This is some pre-work to try and speed up the proof in `hahn_banach`, which as I understand it is super slow because it has to work very hard to unify typeclass which keep switching back and forth between `F` and `restrict_scalars ℝ 𝕜 F`. 

This PR is unlikely to have changed the speed of that proof, but I suspect these definitions might help in a future PR - and it pushes `restrict_scalars` out of the interesting bit of the proof.

Author: eric-wieser

src/analysis/normed_space/extend.lean

@@ -16,6 +16,17 @@ extension is trivial) or `ℂ`. We formulate the extension uniformly, by assumin
 We motivate the form of the extension as follows. Note that `fc : F →ₗ[𝕜] 𝕜` is determined fully by
 `Re fc`: for all `x : F`, `fc (I • x) = I * fc x`, so `Im (fc x) = -Re (fc (I • x))`. Therefore,
 given an `fr : F →ₗ[ℝ] ℝ`, we define `fc x = fr x - fr (I • x) * I`.
+
+## Main definitions
+
+* `linear_map.extend_to_𝕜`
+* `continuous_linear_map.extend_to_𝕜`
+
+## Implementation details
+
+For convenience, the main definitions above operate in terms of `restrict_scalars ℝ 𝕜 F`.
+Alternate forms which operate on `[is_scalar_tower ℝ 𝕜 F]` instead are provided with a primed name.
+
 -/
 
 open is_R_or_C
@@ -25,7 +36,8 @@ local notation `abs𝕜` := @is_R_or_C.abs 𝕜 _
 
 /-- 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_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜 :=
+noncomputable def linear_map.extend_to_𝕜'
+  [semimodule ℝ F] [is_scalar_tower ℝ 𝕜 F] (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,
@@ -40,10 +52,11 @@ begin
   { assume c x,
     rw [← of_real_mul],
     congr' 1,
-    exact fr.map_smul c x },
+    rw [is_R_or_C.of_real_alg, smul_assoc, fr.map_smul, algebra.id.smul_eq_mul, one_smul] },
   have smul_ℝ : ∀ (c : ℝ) (x : F), fc ((c : 𝕜) • x) = (c : 𝕜) * fc x,
   { assume c x,
     simp only [fc, A],
+    rw A c x,
     rw [smul_smul, mul_comm I (c : 𝕜), ← smul_smul, A, mul_sub],
     ring },
   have smul_I : ∀ x : F, fc ((I : 𝕜) • x) = (I : 𝕜) * fc x,
@@ -60,11 +73,15 @@ begin
   exact { to_fun := fc, map_add' := add, map_smul' := smul_𝕜 }
 end
 
+lemma linear_map.extend_to_𝕜'_apply [semimodule ℝ F] [is_scalar_tower ℝ 𝕜 F]
+  (fr : F →ₗ[ℝ] ℝ) (x : F) :
+  fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
+
 /-- The norm of the extension is bounded by `∥fr∥`. -/
-lemma norm_bound (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) (x : F) :
-  ∥fr.to_linear_map.extend_to_𝕜 x∥ ≤ ∥fr∥ * ∥x∥ :=
+lemma norm_bound [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) :
+  ∥(fr.to_linear_map.extend_to_𝕜' x : 𝕜)∥ ≤ ∥fr∥ * ∥x∥ :=
 begin
-  let lm := fr.to_linear_map.extend_to_𝕜,
+  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)
@@ -81,8 +98,8 @@ begin
     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_𝕜, mul_re, I_re, of_real_im, zero_mul,
-        linear_map.coe_mk, add_monoid_hom.map_sub, sub_zero, mul_zero],
+    { 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))
@@ -102,6 +119,26 @@ begin
 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[𝕜] 𝕜 :=
+fr.to_linear_map.extend_to_𝕜'.mk_continuous (∥fr∥) (norm_bound _)
+
+lemma continuous_linear_map.extend_to_𝕜'_apply [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
+  (fr : F →L[ℝ] ℝ) (x : F) :
+  fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
+
+/-- Extend `fr : restrict_scalars ℝ 𝕜 F →ₗ[ℝ] ℝ` to `F →ₗ[𝕜] 𝕜`. -/
+noncomputable def linear_map.extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜 :=
+fr.extend_to_𝕜'
+
+lemma linear_map.extend_to_𝕜_apply (fr : (restrict_scalars ℝ 𝕜 F) →ₗ[ℝ] ℝ) (x : F) :
+  fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
+
+/-- Extend `fr : restrict_scalars ℝ 𝕜 F →L[ℝ] ℝ` to `F →L[𝕜] 𝕜`. -/
 noncomputable def continuous_linear_map.extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) :
   F →L[𝕜] 𝕜 :=
-fr.to_linear_map.extend_to_𝕜.mk_continuous ∥fr∥ (norm_bound _)
+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

src/analysis/normed_space/hahn_banach.lean

@@ -94,8 +94,7 @@ begin
   -- It is an extension of `f`.
   have h : ∀ x : p, g.extend_to_𝕜 x = f x,
   { assume x,
-    change (g (x : F) : 𝕜) - (I : 𝕜) * g ((((I : 𝕜) • x) : p) : F) = f x,
-    rw [hextends, hextends],
+    rw [continuous_linear_map.extend_to_𝕜_apply, ←submodule.coe_smul, hextends, hextends],
     change (re (f x) : 𝕜) - (I : 𝕜) * (re (f ((I : 𝕜) • x))) = f x,
     apply ext,
     { simp only [add_zero, algebra.id.smul_eq_mul, I_re, of_real_im, add_monoid_hom.map_add,