feat(analysis/calculus/fderiv): multiplication by a complex respects real differentiability (#3731)

If `f` takes values in a complex vector space and is real-differentiable, then `c f` is also real-differentiable when `c` is a complex number. This PR proves this fact and the obvious variations, in the general case of two fields where one is a normed algebra over the other one.

Along the way, some material on `module.restrict_scalars` is added, notably in a normed space context.

Author: sgouezel

src/analysis/calculus/fderiv.lean

@@ -2432,9 +2432,8 @@ variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
 {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
 {E : Type*} [normed_group E] [normed_space 𝕜' E]
 {F : Type*} [normed_group F] [normed_space 𝕜' F]
-{f : E → F} {f' : E →L[𝕜'] F} {s : set E} {x : E}
-
-local attribute [instance] normed_space.restrict_scalars
+{f : module.restrict_scalars 𝕜 𝕜' E → module.restrict_scalars 𝕜 𝕜' F}
+{f' : module.restrict_scalars 𝕜 𝕜' E →L[𝕜'] module.restrict_scalars 𝕜 𝕜' F} {s : set E} {x : E}
 
 lemma has_strict_fderiv_at.restrict_scalars (h : has_strict_fderiv_at f f' x) :
   has_strict_fderiv_at f (f'.restrict_scalars 𝕜) x := h
@@ -2462,3 +2461,158 @@ lemma differentiable.restrict_scalars (h : differentiable 𝕜' f) :
 λx, (h x).restrict_scalars 𝕜
 
 end restrict_scalars
+
+/-!
+### Multiplying by a complex function respects real differentiability
+
+Consider two functions `c : E → ℂ` and `f : E → F` where `F` is a complex vector space. If both
+`c` and `f` are differentiable over `ℝ`, then so is their product. This paragraph proves this
+statement, in the general version where `ℝ` is replaced by a field `𝕜`, and `ℂ` is replaced
+by a normed algebra `𝕜'` over `𝕜`.
+ -/
+section smul_algebra
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+{E : Type*} [normed_group E] [normed_space 𝕜 E]
+{F : Type*} [normed_group F] [normed_space 𝕜' F]
+{f : E → module.restrict_scalars 𝕜 𝕜' F}
+{f' : E →L[𝕜] module.restrict_scalars 𝕜 𝕜' F} {s : set E} {x : E}
+{c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} {L : filter E}
+
+theorem has_strict_fderiv_at.smul_algebra (hc : has_strict_fderiv_at c c' x)
+  (hf : has_strict_fderiv_at f f' x) :
+  has_strict_fderiv_at (λ y, c y • f y) (c x • f' + c'.smul_algebra_right (f x)) x :=
+(is_bounded_bilinear_map_smul_algebra.has_strict_fderiv_at (c x, f x)).comp x $
+  hc.prod hf
+
+theorem has_fderiv_within_at.smul_algebra
+  (hc : has_fderiv_within_at c c' s x) (hf : has_fderiv_within_at f f' s x) :
+  has_fderiv_within_at (λ y, c y • f y) (c x • f' + c'.smul_algebra_right (f x)) s x :=
+(is_bounded_bilinear_map_smul_algebra.has_fderiv_at (c x, f x)).comp_has_fderiv_within_at x $
+  hc.prod hf
+
+theorem has_fderiv_at.smul_algebra (hc : has_fderiv_at c c' x) (hf : has_fderiv_at f f' x) :
+  has_fderiv_at (λ y, c y • f y) (c x • f' + c'.smul_algebra_right (f x)) x :=
+(is_bounded_bilinear_map_smul_algebra.has_fderiv_at (c x, f x)).comp x $
+  hc.prod hf
+
+lemma differentiable_within_at.smul_algebra
+  (hc : differentiable_within_at 𝕜 c s x) (hf : differentiable_within_at 𝕜 f s x) :
+  differentiable_within_at 𝕜 (λ y, c y • f y) s x :=
+(hc.has_fderiv_within_at.smul_algebra hf.has_fderiv_within_at).differentiable_within_at
+
+@[simp] lemma differentiable_at.smul_algebra
+  (hc : differentiable_at 𝕜 c x) (hf : differentiable_at 𝕜 f x) :
+  differentiable_at 𝕜 (λ y, c y • f y) x :=
+(hc.has_fderiv_at.smul_algebra hf.has_fderiv_at).differentiable_at
+
+lemma differentiable_on.smul_algebra (hc : differentiable_on 𝕜 c s) (hf : differentiable_on 𝕜 f s) :
+  differentiable_on 𝕜 (λ y, c y • f y) s :=
+λx hx, (hc x hx).smul_algebra (hf x hx)
+
+@[simp] lemma differentiable.smul_algebra (hc : differentiable 𝕜 c) (hf : differentiable 𝕜 f) :
+  differentiable 𝕜 (λ y, c y • f y) :=
+λx, (hc x).smul_algebra (hf x)
+
+lemma fderiv_within_smul_algebra (hxs : unique_diff_within_at 𝕜 s x)
+  (hc : differentiable_within_at 𝕜 c s x) (hf : differentiable_within_at 𝕜 f s x) :
+  fderiv_within 𝕜 (λ y, c y • f y) s x =
+    c x • fderiv_within 𝕜 f s x + (fderiv_within 𝕜 c s x).smul_algebra_right (f x) :=
+(hc.has_fderiv_within_at.smul_algebra hf.has_fderiv_within_at).fderiv_within hxs
+
+lemma fderiv_smul_algebra (hc : differentiable_at 𝕜 c x) (hf : differentiable_at 𝕜 f x) :
+  fderiv 𝕜 (λ y, c y • f y) x =
+    c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smul_algebra_right (f x) :=
+(hc.has_fderiv_at.smul_algebra hf.has_fderiv_at).fderiv
+
+theorem has_strict_fderiv_at.smul_algebra_const
+  (hc : has_strict_fderiv_at c c' x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  has_strict_fderiv_at (λ y, c y • f) (c'.smul_algebra_right f) x :=
+by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_strict_fderiv_at_const f x)
+
+theorem has_fderiv_within_at.smul_algebra_const
+  (hc : has_fderiv_within_at c c' s x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  has_fderiv_within_at (λ y, c y • f) (c'.smul_algebra_right f) s x :=
+by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_fderiv_within_at_const f x s)
+
+theorem has_fderiv_at.smul_algebra_const
+  (hc : has_fderiv_at c c' x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  has_fderiv_at (λ y, c y • f) (c'.smul_algebra_right f) x :=
+by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_fderiv_at_const f x)
+
+lemma differentiable_within_at.smul_algebra_const
+  (hc : differentiable_within_at 𝕜 c s x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  differentiable_within_at 𝕜 (λ y, c y • f) s x :=
+(hc.has_fderiv_within_at.smul_algebra_const f).differentiable_within_at
+
+lemma differentiable_at.smul_algebra_const
+  (hc : differentiable_at 𝕜 c x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  differentiable_at 𝕜 (λ y, c y • f) x :=
+(hc.has_fderiv_at.smul_algebra_const f).differentiable_at
+
+lemma differentiable_on.smul_algebra_const
+  (hc : differentiable_on 𝕜 c s) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  differentiable_on 𝕜 (λ y, c y • f) s :=
+λx hx, (hc x hx).smul_algebra_const f
+
+lemma differentiable.smul_algebra_const
+  (hc : differentiable 𝕜 c) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  differentiable 𝕜 (λ y, c y • f) :=
+λx, (hc x).smul_algebra_const f
+
+lemma fderiv_within_smul_algebra_const (hxs : unique_diff_within_at 𝕜 s x)
+  (hc : differentiable_within_at 𝕜 c s x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  fderiv_within 𝕜 (λ y, c y • f) s x =
+    (fderiv_within 𝕜 c s x).smul_algebra_right f :=
+(hc.has_fderiv_within_at.smul_algebra_const f).fderiv_within hxs
+
+lemma fderiv_smul_algebra_const
+  (hc : differentiable_at 𝕜 c x) (f : module.restrict_scalars 𝕜 𝕜' F) :
+  fderiv 𝕜 (λ y, c y • f) x = (fderiv 𝕜 c x).smul_algebra_right f :=
+(hc.has_fderiv_at.smul_algebra_const f).fderiv
+
+theorem has_strict_fderiv_at.const_smul_algebra (h : has_strict_fderiv_at f f' x) (c : 𝕜') :
+  has_strict_fderiv_at (λ x, c • f x) (c • f') x :=
+(c • (1 : (module.restrict_scalars 𝕜 𝕜' F) →L[𝕜] ((module.restrict_scalars 𝕜 𝕜' F))))
+  .has_strict_fderiv_at.comp x h
+
+theorem has_fderiv_at_filter.const_smul_algebra (h : has_fderiv_at_filter f f' x L) (c : 𝕜') :
+  has_fderiv_at_filter (λ x, c • f x) (c • f') x L :=
+(c • (1 : (module.restrict_scalars 𝕜 𝕜' F) →L[𝕜] ((module.restrict_scalars 𝕜 𝕜' F))))
+  .has_fderiv_at_filter.comp x h
+
+theorem has_fderiv_within_at.const_smul_algebra (h : has_fderiv_within_at f f' s x) (c : 𝕜') :
+  has_fderiv_within_at (λ x, c • f x) (c • f') s x :=
+h.const_smul_algebra c
+
+theorem has_fderiv_at.const_smul_algebra (h : has_fderiv_at f f' x) (c : 𝕜') :
+  has_fderiv_at (λ x, c • f x) (c • f') x :=
+h.const_smul_algebra c
+
+lemma differentiable_within_at.const_smul_algebra (h : differentiable_within_at 𝕜 f s x) (c : 𝕜') :
+  differentiable_within_at 𝕜 (λy, c • f y) s x :=
+(h.has_fderiv_within_at.const_smul_algebra c).differentiable_within_at
+
+lemma differentiable_at.const_smul_algebra (h : differentiable_at 𝕜 f x) (c : 𝕜') :
+  differentiable_at 𝕜 (λy, c • f y) x :=
+(h.has_fderiv_at.const_smul_algebra c).differentiable_at
+
+lemma differentiable_on.const_smul_algebra (h : differentiable_on 𝕜 f s) (c : 𝕜') :
+  differentiable_on 𝕜 (λy, c • f y) s :=
+λx hx, (h x hx).const_smul_algebra c
+
+lemma differentiable.const_smul_algebra (h : differentiable 𝕜 f) (c : 𝕜') :
+  differentiable 𝕜 (λy, c • f y) :=
+λx, (h x).const_smul_algebra c
+
+lemma fderiv_within_const_smul_algebra (hxs : unique_diff_within_at 𝕜 s x)
+  (h : differentiable_within_at 𝕜 f s x) (c : 𝕜') :
+  fderiv_within 𝕜 (λy, c • f y) s x = c • fderiv_within 𝕜 f s x :=
+(h.has_fderiv_within_at.const_smul_algebra c).fderiv_within hxs
+
+lemma fderiv_const_smul_algebra (h : differentiable_at 𝕜 f x) (c : 𝕜') :
+  fderiv 𝕜 (λy, c • f y) x = c • fderiv 𝕜 f x :=
+(h.has_fderiv_at.const_smul_algebra c).fderiv
+
+end smul_algebra

src/analysis/complex/basic.lean

@@ -75,9 +75,16 @@ finite_dimensional.proper ℂ E
 attribute [instance, priority 900] complex.finite_dimensional.proper
 
 /-- A complex normed vector space is also a real normed vector space. -/
+@[priority 900]
 instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed_space ℂ E] :
-  normed_space ℝ E := normed_space.restrict_scalars ℝ ℂ
-attribute [instance, priority 900] complex.normed_space.restrict_scalars_real
+  normed_space ℝ E := normed_space.restrict_scalars' ℝ ℂ E
+
+/-- The space of continuous linear maps over `ℝ`, from a real vector space to a complex vector
+space, is a normed vector space over `ℂ`. -/
+instance continuous_linear_map.real_smul_complex (E : Type*) [normed_group E] [normed_space ℝ E]
+  (F : Type*) [normed_group F] [normed_space ℂ F] :
+  normed_space ℂ (E →L[ℝ] F) :=
+continuous_linear_map.normed_space_extend_scalars
 
 /-- Linear map version of the real part function, from `ℂ` to `ℝ`. -/
 def linear_map.re : ℂ →ₗ[ℝ] ℝ :=

src/analysis/normed_space/basic.lean

@@ -984,19 +984,30 @@ end normed_algebra
 section restrict_scalars
 
 variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
-{E : Type*} [normed_group E] [normed_space 𝕜' E]
+(E : Type*) [normed_group E] [normed_space 𝕜' E]
 
 /-- `𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
-normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred. -/
--- We could add a type synonym equipped with this as an instance,
--- as we've done for `module.restrict_scalars`.
-def normed_space.restrict_scalars : normed_space 𝕜 E :=
+normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred.
+
+The type synonym `module.restrict_scalars 𝕜 𝕜' E` will be endowed with this instance by default.
+-/
+def normed_space.restrict_scalars' : normed_space 𝕜 E :=
 { norm_smul_le := λc x, le_of_eq $ begin
     change ∥(algebra_map 𝕜 𝕜' c) • x∥ = ∥c∥ * ∥x∥,
     simp [norm_smul]
   end,
   ..module.restrict_scalars' 𝕜 𝕜' E }
 
+instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : normed_group E] :
+  normed_group (module.restrict_scalars 𝕜 𝕜' E) := I
+
+instance module.restrict_scalars.normed_space_orig {𝕜 : Type*} {𝕜' : Type*} {E : Type*}
+  [normed_field 𝕜'] [normed_group E] [I : normed_space 𝕜' E] :
+  normed_space 𝕜' (module.restrict_scalars 𝕜 𝕜' E) := I
+
+instance : normed_space 𝕜 (module.restrict_scalars 𝕜 𝕜' E) :=
+(normed_space.restrict_scalars' 𝕜 𝕜' E : normed_space 𝕜 E)
+
 end restrict_scalars
 
 section summable

src/analysis/normed_space/bounded_linear_maps.lean

@@ -278,6 +278,15 @@ lemma is_bounded_bilinear_map_smul :
   smul_right := λc x y, by simp [smul_smul, mul_comm],
   bound      := ⟨1, zero_lt_one, λx y, by simp [norm_smul]⟩ }
 
+lemma is_bounded_bilinear_map_smul_algebra {𝕜' : Type*} [normed_field 𝕜']
+  [normed_algebra 𝕜 𝕜'] {E : Type*} [normed_group E] [normed_space 𝕜' E] :
+  is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × (module.restrict_scalars 𝕜 𝕜' E)), p.1 • p.2) :=
+{ add_left   := add_smul,
+  smul_left  := λ c x y, by simp [smul_algebra_smul],
+  add_right  := smul_add,
+  smul_right := λ c x y, by simp [smul_algebra_smul, smul_algebra_smul_comm],
+  bound      := ⟨1, zero_lt_one, λ x y, by simp [norm_smul] ⟩ }
+
 lemma is_bounded_bilinear_map_mul :
   is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.1 * p.2) :=
 is_bounded_bilinear_map_smul

src/analysis/normed_space/hahn_banach.lean

@@ -52,7 +52,7 @@ variables {F : Type*} [normed_group F] [normed_space ℂ F]
 -- Inlining the following two definitions causes a type mismatch between
 -- subspace ℝ (module.restrict_scalars ℝ ℂ F) and subspace ℂ F.
 /-- Restrict a ℂ-subspace to an ℝ-subspace. -/
-noncomputable def restrict_scalars (p: subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ ℂ F
+noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ ℂ F
 
 private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) :
   ∃ g : F →L[ℝ] ℝ, (∀ x : restrict_scalars p, g x = f' x) ∧ ∥g∥ = ∥f'∥ :=

src/analysis/normed_space/operator_norm.lean

@@ -581,6 +581,16 @@ end uniformly_extend
 
 end op_norm
 
+end continuous_linear_map
+
+/-- If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`,
+then its norm is bounded by the bound given to the constructor if it is nonnegative. -/
+lemma linear_map.mk_continuous_norm_le (f : E →ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
+  ∥f.mk_continuous C h∥ ≤ C :=
+continuous_linear_map.op_norm_le_bound _ hC h
+
+namespace continuous_linear_map
+
 /-- The norm of the tensor product of a scalar linear map and of an element of a normed space
 is the product of the norms. -/
 @[simp] lemma smul_right_norm {c : E →L[𝕜] 𝕜} {f : F} :
@@ -636,38 +646,82 @@ variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
 {E' : Type*} [normed_group E'] [normed_space 𝕜' E']
 {F' : Type*} [normed_group F'] [normed_space 𝕜' F']
 
-local attribute [instance, priority 500] normed_space.restrict_scalars
-
 /-- `𝕜`-linear continuous function induced by a `𝕜'`-linear continuous function when `𝕜'` is a
 normed algebra over `𝕜`. -/
-def restrict_scalars (f : E' →L[𝕜'] F') : E' →L[𝕜] F' :=
+def restrict_scalars (f : E' →L[𝕜'] F') :
+  (module.restrict_scalars 𝕜 𝕜' E') →L[𝕜] (module.restrict_scalars 𝕜 𝕜' F') :=
 { cont := f.cont,
   ..linear_map.restrict_scalars 𝕜 (f.to_linear_map) }
 
 @[simp, norm_cast] lemma restrict_scalars_coe_eq_coe (f : E' →L[𝕜'] F') :
-  (f.restrict_scalars 𝕜 : E' →ₗ[𝕜] F') = (f : E' →ₗ[𝕜'] F').restrict_scalars 𝕜 := rfl
+  (f.restrict_scalars 𝕜 :
+    (module.restrict_scalars 𝕜 𝕜' E') →ₗ[𝕜] (module.restrict_scalars 𝕜 𝕜' F')) =
+  (f : E' →ₗ[𝕜'] F').restrict_scalars 𝕜 := rfl
 
 @[simp, norm_cast squash] lemma restrict_scalars_coe_eq_coe' (f : E' →L[𝕜'] F') :
   (f.restrict_scalars 𝕜 : E' → F') = f := rfl
 
 end restrict_scalars
 
-end continuous_linear_map
+section extend_scalars
+
+variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+{F' : Type*} [normed_group F'] [normed_space 𝕜' F']
+
+instance has_scalar_extend_scalars : has_scalar 𝕜' (E →L[𝕜] (module.restrict_scalars 𝕜 𝕜' F')) :=
+{ smul := λ c f, (c • f.to_linear_map).mk_continuous (∥c∥ * ∥f∥)
+begin
+  assume x,
+  calc ∥c • (f x)∥ = ∥c∥ * ∥f x∥ : norm_smul c _
+  ... ≤ ∥c∥ * (∥f∥ * ∥x∥) : mul_le_mul_of_nonneg_left (le_op_norm f x) (norm_nonneg _)
+  ... = ∥c∥ * ∥f∥ * ∥x∥ : (mul_assoc _ _ _).symm
+end }
+
+instance module_extend_scalars : module 𝕜' (E →L[𝕜] (module.restrict_scalars 𝕜 𝕜' F')) :=
+{ smul_zero := λ _, ext $ λ _, smul_zero _,
+  zero_smul := λ _, ext $ λ _, zero_smul _ _,
+  one_smul  := λ _, ext $ λ _, one_smul _ _,
+  mul_smul  := λ _ _ _, ext $ λ _, mul_smul _ _ _,
+  add_smul  := λ _ _ _, ext $ λ _, add_smul _ _ _,
+  smul_add  := λ _ _ _, ext $ λ _, smul_add _ _ _ }
+
+instance normed_space_extend_scalars : normed_space 𝕜' (E →L[𝕜] (module.restrict_scalars 𝕜 𝕜' F')) :=
+{ norm_smul_le := λ c f,
+    linear_map.mk_continuous_norm_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _ }
+
+/-- When `f` is a continuous linear map taking values in `S`, then `λb, f b • x` is a
+continuous linear map. -/
+def smul_algebra_right (f : E →L[𝕜] 𝕜') (x : module.restrict_scalars 𝕜 𝕜' F') :
+  E →L[𝕜] (module.restrict_scalars 𝕜 𝕜' F') :=
+{ cont := by continuity!,
+  .. smul_algebra_right f.to_linear_map x }
+
+@[simp] theorem smul_algebra_right_apply
+  (f : E →L[𝕜] 𝕜') (x : module.restrict_scalars 𝕜 𝕜' F') (c : E) :
+  smul_algebra_right f x c = f c • x := rfl
+
+end extend_scalars
+
+section has_sum
 
 variables {ι : Type*}
 
 /-- Applying a continuous linear map commutes with taking an (infinite) sum. -/
-lemma continuous_linear_map.has_sum {f : ι → E} (φ : E →L[𝕜] F) {x : E} (hf : has_sum f x) :
+protected lemma has_sum {f : ι → E} (φ : E →L[𝕜] F) {x : E} (hf : has_sum f x) :
   has_sum (λ (b:ι), φ (f b)) (φ x) :=
 begin
   unfold has_sum,
   convert φ.continuous.continuous_at.tendsto.comp hf,
   ext s, rw [function.comp_app, finset.sum_hom s φ],
 end
 
-lemma continuous_linear_map.has_sum_of_summable {f : ι → E} (φ : E →L[𝕜] F) (hf : summable f) :
+lemma has_sum_of_summable {f : ι → E} (φ : E →L[𝕜] F) (hf : summable f) :
   has_sum (λ (b:ι), φ (f b)) (φ (∑'b, f b)) :=
-continuous_linear_map.has_sum φ hf.has_sum
+φ.has_sum hf.has_sum
+
+end has_sum
+
+end continuous_linear_map
 
 namespace continuous_linear_equiv
 
@@ -832,12 +886,6 @@ continuous_linear_equiv.uniform_embedding
   continuous_inv_fun := h₂,
   .. e }
 
-/-- If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`,
-then its norm is bounded by the bound given to the constructor if it is nonnegative. -/
-lemma linear_map.mk_continuous_norm_le (f : E →ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
-  ∥f.mk_continuous C h∥ ≤ C :=
-continuous_linear_map.op_norm_le_bound _ hC h
-
 namespace continuous_linear_map
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 

src/data/complex/module.lean

@@ -6,9 +6,11 @@ Authors: Alexander Bentkamp, Sébastien Gouëzel
 import data.complex.basic
 import ring_theory.algebra
 /-!
-This file contains two instance, the fact the ℂ is an ℝ algebra,
-and an instance to view any complex vector space as a
-real vector space
+This file contains three instances:
+* `ℂ` is an `ℝ` algebra;
+* any complex vector space is a real vector space;
+* the space of `ℝ`-linear maps from a real vector space to a complex vector space is a complex
+  vector space.
 -/
 noncomputable theory
 
@@ -23,3 +25,7 @@ vector space. -/
 instance module.complex_to_real (E : Type*) [add_comm_group E] [module ℂ E] : module ℝ E :=
 module.restrict_scalars' ℝ ℂ E
 attribute [instance, priority 900] module.complex_to_real
+
+instance (E : Type*) [add_comm_group E] [module ℝ E]
+  (F : Type*) [add_comm_group F] [module ℂ F] : module ℂ (E →ₗ[ℝ] F) :=
+linear_map.module_extend_scalars _ _ _ _