feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real (#6621)

Add continuous linear maps and linear isometries (when applicable) for the following `is_R_or_C` functions: `re`, `im`, `conj` and `of_real`.
Rename the existing continuous linear maps defined in complex.basic to adopt the naming convention of is_R_or_C.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: RemyDegenne

src/analysis/complex/basic.lean

@@ -17,12 +17,14 @@ This file registers `ℂ` as a normed field, expresses basic properties of the n
 tools on the real vector space structure of `ℂ`. Notably, in the namespace `complex`,
 it defines functions:
 
-* `continuous_linear_map.re`
-* `continuous_linear_map.im`
-* `continuous_linear_map.of_real`
+* `re_clm`
+* `im_clm`
+* `of_real_clm`
+* `conj_clm`
 
-They are bundled versions of the real part, the imaginary part, and the embedding of `ℝ` in `ℂ`,
-as continuous `ℝ`-linear maps.
+They are bundled versions of the real part, the imaginary part, the embedding of `ℝ` in `ℂ`, and
+the complex conjugate as continuous `ℝ`-linear maps. The last two are also bundled as linear
+isometries in `of_real_li` and `conj_li`.
 
 We also register the fact that `ℂ` is an `is_R_or_C` field.
 -/
@@ -74,80 +76,64 @@ by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.re : ℂ →L[ℝ] ℝ :=
-linear_map.re.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_re_le_abs])
+def re_clm : ℂ →L[ℝ] ℝ := re_lm.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_re_le_abs])
 
-@[continuity] lemma continuous_re : continuous re := continuous_linear_map.re.continuous
+@[continuity] lemma continuous_re : continuous re := re_clm.continuous
 
-@[simp] lemma continuous_linear_map.re_coe :
-  (coe (continuous_linear_map.re) : ℂ →ₗ[ℝ] ℝ) = linear_map.re := rfl
+@[simp] lemma re_clm_coe : (coe (re_clm) : ℂ →ₗ[ℝ] ℝ) = re_lm := rfl
 
-@[simp] lemma continuous_linear_map.re_apply (z : ℂ) :
-  (continuous_linear_map.re : ℂ → ℝ) z = z.re := rfl
+@[simp] lemma re_clm_apply (z : ℂ) : (re_clm : ℂ → ℝ) z = z.re := rfl
 
-@[simp] lemma continuous_linear_map.re_norm :
-  ∥continuous_linear_map.re∥ = 1 :=
+@[simp] lemma re_clm_norm : ∥re_clm∥ = 1 :=
 le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
-calc 1 = ∥continuous_linear_map.re 1∥ : by simp
-   ... ≤ ∥continuous_linear_map.re∥ : unit_le_op_norm _ _ (by simp)
+calc 1 = ∥re_clm 1∥ : by simp
+   ... ≤ ∥re_clm∥ : unit_le_op_norm _ _ (by simp)
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.im : ℂ →L[ℝ] ℝ :=
-linear_map.im.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_im_le_abs])
+def im_clm : ℂ →L[ℝ] ℝ := im_lm.mk_continuous 1 (λ x, by simp [real.norm_eq_abs, abs_im_le_abs])
 
-@[continuity] lemma continuous_im : continuous im := continuous_linear_map.im.continuous
+@[continuity] lemma continuous_im : continuous im := im_clm.continuous
 
-@[simp] lemma continuous_linear_map.im_coe :
-  (coe (continuous_linear_map.im) : ℂ →ₗ[ℝ] ℝ) = linear_map.im := rfl
+@[simp] lemma im_clm_coe : (coe (im_clm) : ℂ →ₗ[ℝ] ℝ) = im_lm := rfl
 
-@[simp] lemma continuous_linear_map.im_apply (z : ℂ) :
-  (continuous_linear_map.im : ℂ → ℝ) z = z.im := rfl
+@[simp] lemma im_clm_apply (z : ℂ) : (im_clm : ℂ → ℝ) z = z.im := rfl
 
-@[simp] lemma continuous_linear_map.im_norm :
-  ∥continuous_linear_map.im∥ = 1 :=
+@[simp] lemma im_clm_norm : ∥im_clm∥ = 1 :=
 le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _) $
-calc 1 = ∥continuous_linear_map.im I∥ : by simp
-   ... ≤ ∥continuous_linear_map.im∥ : unit_le_op_norm _ _ (by simp)
+calc 1 = ∥im_clm I∥ : by simp
+   ... ≤ ∥im_clm∥ : unit_le_op_norm _ _ (by simp)
 
 /-- The complex-conjugation function from `ℂ` to itself is an isometric linear map. -/
-def linear_isometry.conj : ℂ →ₗᵢ[ℝ] ℂ := ⟨linear_map.conj, λ x, by simp⟩
+def conj_li : ℂ →ₗᵢ[ℝ] ℂ := ⟨conj_lm, λ x, by simp⟩
 
 /-- Continuous linear map version of the conj function, from `ℂ` to `ℂ`. -/
-def continuous_linear_map.conj : ℂ →L[ℝ] ℂ := linear_isometry.conj.to_continuous_linear_map
+def conj_clm : ℂ →L[ℝ] ℂ := conj_li.to_continuous_linear_map
 
-lemma isometry_conj : isometry (conj : ℂ → ℂ) := linear_isometry.conj.isometry
+lemma isometry_conj : isometry (conj : ℂ → ℂ) := conj_li.isometry
 
-@[continuity] lemma continuous_conj : continuous conj := continuous_linear_map.conj.continuous
+@[continuity] lemma continuous_conj : continuous conj := conj_clm.continuous
 
-@[simp] lemma continuous_linear_map.conj_coe :
-  (coe (continuous_linear_map.conj) : ℂ →ₗ[ℝ] ℂ) = linear_map.conj := rfl
+@[simp] lemma conj_clm_coe : (coe (conj_clm) : ℂ →ₗ[ℝ] ℂ) = conj_lm := rfl
 
-@[simp] lemma continuous_linear_map.conj_apply (z : ℂ) :
-  (continuous_linear_map.conj : ℂ → ℂ) z = z.conj := rfl
+@[simp] lemma conj_clm_apply (z : ℂ) : (conj_clm : ℂ → ℂ) z = z.conj := rfl
 
-@[simp] lemma continuous_linear_map.conj_norm :
-  ∥continuous_linear_map.conj∥ = 1 :=
-linear_isometry.conj.norm_to_continuous_linear_map
+@[simp] lemma conj_clm_norm : ∥conj_clm∥ = 1 := conj_li.norm_to_continuous_linear_map
 
 /-- Linear isometry version of the canonical embedding of `ℝ` in `ℂ`. -/
-def linear_isometry.of_real : ℝ →ₗᵢ[ℝ] ℂ := ⟨linear_map.of_real, λ x, by simp⟩
+def of_real_li : ℝ →ₗᵢ[ℝ] ℂ := ⟨of_real_lm, λ x, by simp⟩
 
 /-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
-def continuous_linear_map.of_real : ℝ →L[ℝ] ℂ := linear_isometry.of_real.to_continuous_linear_map
+def of_real_clm : ℝ →L[ℝ] ℂ := of_real_li.to_continuous_linear_map
 
-lemma isometry_of_real : isometry (coe : ℝ → ℂ) := linear_isometry.of_real.isometry
+lemma isometry_of_real : isometry (coe : ℝ → ℂ) := of_real_li.isometry
 
 @[continuity] lemma continuous_of_real : continuous (coe : ℝ → ℂ) := isometry_of_real.continuous
 
-@[simp] lemma continuous_linear_map.of_real_coe :
-  (coe (continuous_linear_map.of_real) : ℝ →ₗ[ℝ] ℂ) = linear_map.of_real := rfl
+@[simp] lemma of_real_clm_coe : (coe (of_real_clm) : ℝ →ₗ[ℝ] ℂ) = of_real_lm := rfl
 
-@[simp] lemma continuous_linear_map.of_real_apply (x : ℝ) :
-  (continuous_linear_map.of_real : ℝ → ℂ) x = x := rfl
+@[simp] lemma of_real_clm_apply (x : ℝ) : (of_real_clm : ℝ → ℂ) x = x := rfl
 
-@[simp] lemma continuous_linear_map.of_real_norm :
-  ∥continuous_linear_map.of_real∥ = 1 :=
-linear_isometry.of_real.norm_to_continuous_linear_map
+@[simp] lemma of_real_clm_norm : ∥of_real_clm∥ = 1 := of_real_li.norm_to_continuous_linear_map
 
 noncomputable instance : is_R_or_C ℂ :=
 { re := ⟨complex.re, complex.zero_re, complex.add_re⟩,

src/analysis/complex/real_deriv.lean

@@ -24,14 +24,12 @@ differentiable at this point, with a derivative equal to the real part of the co
 theorem has_strict_deriv_at.real_of_complex (h : has_strict_deriv_at e e' z) :
   has_strict_deriv_at (λx:ℝ, (e x).re) e'.re z :=
 begin
-  have A : has_strict_fderiv_at (coe : ℝ → ℂ) continuous_linear_map.of_real z :=
-    continuous_linear_map.of_real.has_strict_fderiv_at,
+  have A : has_strict_fderiv_at (coe : ℝ → ℂ) of_real_clm z := of_real_clm.has_strict_fderiv_at,
   have B : has_strict_fderiv_at e
     ((continuous_linear_map.smul_right 1 e' : ℂ →L[ℂ] ℂ).restrict_scalars ℝ)
-    (continuous_linear_map.of_real z) :=
+    (of_real_clm z) :=
     h.has_strict_fderiv_at.restrict_scalars ℝ,
-  have C : has_strict_fderiv_at re continuous_linear_map.re (e (continuous_linear_map.of_real z)) :=
-    continuous_linear_map.re.has_strict_fderiv_at,
+  have C : has_strict_fderiv_at re re_clm (e (of_real_clm z)) := re_clm.has_strict_fderiv_at,
   simpa using (C.comp z (B.comp z A)).has_strict_deriv_at
 end
 
@@ -40,24 +38,21 @@ differentiable at this point, with a derivative equal to the real part of the co
 theorem has_deriv_at.real_of_complex (h : has_deriv_at e e' z) :
   has_deriv_at (λx:ℝ, (e x).re) e'.re z :=
 begin
-  have A : has_fderiv_at (coe : ℝ → ℂ) continuous_linear_map.of_real z :=
-    continuous_linear_map.of_real.has_fderiv_at,
+  have A : has_fderiv_at (coe : ℝ → ℂ) of_real_clm z := of_real_clm.has_fderiv_at,
   have B : has_fderiv_at e ((continuous_linear_map.smul_right 1 e' : ℂ →L[ℂ] ℂ).restrict_scalars ℝ)
-    (continuous_linear_map.of_real z) :=
+    (of_real_clm z) :=
     h.has_fderiv_at.restrict_scalars ℝ,
-  have C : has_fderiv_at re continuous_linear_map.re (e (continuous_linear_map.of_real z)) :=
-    continuous_linear_map.re.has_fderiv_at,
+  have C : has_fderiv_at re re_clm (e (of_real_clm z)) := re_clm.has_fderiv_at,
   simpa using (C.comp z (B.comp z A)).has_deriv_at
 end
 
 theorem times_cont_diff_at.real_of_complex {n : with_top ℕ} (h : times_cont_diff_at ℂ n e z) :
   times_cont_diff_at ℝ n (λ x : ℝ, (e x).re) z :=
 begin
   have A : times_cont_diff_at ℝ n (coe : ℝ → ℂ) z,
-    from continuous_linear_map.of_real.times_cont_diff.times_cont_diff_at,
+    from of_real_clm.times_cont_diff.times_cont_diff_at,
   have B : times_cont_diff_at ℝ n e z := h.restrict_scalars ℝ,
-  have C : times_cont_diff_at ℝ n re (e z),
-    from continuous_linear_map.re.times_cont_diff.times_cont_diff_at,
+  have C : times_cont_diff_at ℝ n re (e z), from re_clm.times_cont_diff.times_cont_diff_at,
   exact C.comp z (B.comp z A)
 end
 

src/analysis/normed_space/hahn_banach.lean

@@ -111,7 +111,7 @@ begin
         ≤ ∥g∥ : g.extend_to_𝕜.op_norm_le_bound g.op_norm_nonneg (norm_bound _)
     ... = ∥fr∥ : hnormeq
     ... ≤ ∥re_clm∥ * ∥f∥ : continuous_linear_map.op_norm_comp_le _ _
-    ... = ∥f∥ : by rw [norm_re_clm, one_mul] },
+    ... = ∥f∥ : by rw [re_clm_norm, one_mul] },
   { exact f.op_norm_le_bound g.extend_to_𝕜.op_norm_nonneg (λ x, h x ▸ g.extend_to_𝕜.le_op_norm x) },
 end
 

src/data/complex/is_R_or_C.lean

@@ -144,6 +144,9 @@ end
 ext_iff.2 $ by simp
 @[simp, norm_cast, priority 900] lemma of_real_mul (r s : ℝ) : ((r * s : ℝ) : K) = r * s :=
 ext_iff.2 $ by simp
+@[simp, norm_cast] lemma of_real_smul (r x : ℝ) : r • (x : K) = (r : K) * (x : K) :=
+by { simp_rw [← smul_eq_mul, of_real_alg r], simp, }
+
 lemma of_real_mul_re (r : ℝ) (z : K) : re (↑r * z) = r * re z :=
 by simp only [mul_re, of_real_im, zero_mul, of_real_re, sub_zero]
 lemma of_real_mul_im (r : ℝ) (z : K) : im (↑r * z) = r * (im z) :=
@@ -154,12 +157,6 @@ lemma smul_re : ∀ (r : ℝ) (z : K), re (r • z) = r * (re z) :=
 lemma smul_im : ∀ (r : ℝ) (z : K), im (r • z) = r * (im z) :=
 λ r z, by { rw algebra.smul_def, apply of_real_mul_im }
 
-/-- The real part in a `is_R_or_C` field, as a linear map. -/
-noncomputable def re_lm : K →ₗ[ℝ] ℝ :=
-{ map_smul' := smul_re,  .. re }
-
-@[simp] lemma re_lm_coe : (re_lm : K → ℝ) = re := rfl
-
 /-! ### The imaginary unit, `I` -/
 
 /-- The imaginary unit. -/
@@ -195,6 +192,17 @@ lemma conj_inj (z w : K) : conj z = conj w ↔ z = w := conj_bijective.1.eq_iff
 lemma conj_eq_zero {z : K} : conj z = 0 ↔ z = 0 :=
 ring_hom.map_eq_zero conj
 
+lemma conj_eq_re_sub_im (z : K) : conj z = re z - (im z) * I := by { rw ext_iff, simp, }
+
+lemma conj_smul (r : ℝ) (z : K) : conj (r • z) = r • conj z :=
+begin
+  simp_rw conj_eq_re_sub_im,
+  simp only [smul_re, smul_im, of_real_mul],
+  rw smul_sub,
+  simp_rw of_real_alg,
+  simp,
+end
+
 lemma eq_conj_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
 begin
   split,
@@ -563,21 +571,6 @@ begin
   simp [of_real_im, mul_im, conj_im, conj_re, mul_comm],
 end
 
-/-- The real part in a `is_R_or_C` field, as a continuous linear map. -/
-noncomputable def re_clm : K →L[ℝ] ℝ :=
-re_lm.mk_continuous 1 $ by { simp only [norm_eq_abs, re_lm_coe, one_mul], exact abs_re_le_abs }
-
-@[simp] lemma norm_re_clm : ∥(re_clm : K →L[ℝ] ℝ)∥ = 1 :=
-begin
-  apply le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _),
-  convert continuous_linear_map.ratio_le_op_norm _ (1 : K),
-  simp,
-end
-
-@[simp, norm_cast] lemma re_clm_coe : ((re_clm : K →L[ℝ] ℝ) : K →ₗ[ℝ] ℝ) = re_lm := rfl
-
-@[simp] lemma re_clm_apply : ((re_clm : K →L[ℝ] ℝ) : K → ℝ) = re := rfl
-
 /-! ### Cauchy sequences -/
 
 theorem is_cau_seq_re (f : cau_seq K abs) : is_cau_seq abs' (λ n, re (f n)) :=
@@ -707,6 +700,100 @@ by simp [is_R_or_C.abs, abs, real.sqrt_mul_self_eq_abs]
 
 end cleanup_lemmas
 
+section linear_maps
+
+variables {K : Type*} [is_R_or_C K]
+
+/-- The real part in a `is_R_or_C` field, as a linear map. -/
+noncomputable def re_lm : K →ₗ[ℝ] ℝ :=
+{ map_smul' := smul_re,  .. re }
+
+@[simp] lemma re_lm_coe : (re_lm : K → ℝ) = re := rfl
+
+/-- The real part in a `is_R_or_C` field, as a continuous linear map. -/
+noncomputable def re_clm : K →L[ℝ] ℝ :=
+re_lm.mk_continuous 1 $ by
+{ simp only [norm_eq_abs, re_lm_coe, one_mul, abs_to_real], exact abs_re_le_abs, }
+
+@[simp] lemma re_clm_norm : ∥(re_clm : K →L[ℝ] ℝ)∥ = 1 :=
+begin
+  apply le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _),
+  convert continuous_linear_map.ratio_le_op_norm _ (1 : K),
+  simp,
+end
+
+@[simp, norm_cast] lemma re_clm_coe : ((re_clm : K →L[ℝ] ℝ) : K →ₗ[ℝ] ℝ) = re_lm := rfl
+
+@[simp] lemma re_clm_apply : ((re_clm : K →L[ℝ] ℝ) : K → ℝ) = re := rfl
+
+@[continuity] lemma continuous_re : continuous (re : K → ℝ) := re_clm.continuous
+
+/-- The imaginary part in a `is_R_or_C` field, as a linear map. -/
+noncomputable def im_lm : K →ₗ[ℝ] ℝ :=
+{ map_smul' := smul_im,  .. im }
+
+@[simp] lemma im_lm_coe : (im_lm : K → ℝ) = im := rfl
+
+/-- The imaginary part in a `is_R_or_C` field, as a continuous linear map. -/
+noncomputable def im_clm : K →L[ℝ] ℝ :=
+im_lm.mk_continuous 1 $ by
+{ simp only [norm_eq_abs, re_lm_coe, one_mul, abs_to_real], exact abs_im_le_abs, }
+
+@[simp, norm_cast] lemma im_clm_coe : ((im_clm : K →L[ℝ] ℝ) : K →ₗ[ℝ] ℝ) = im_lm := rfl
+
+@[simp] lemma im_clm_apply : ((im_clm : K →L[ℝ] ℝ) : K → ℝ) = im := rfl
+
+@[continuity] lemma continuous_im : continuous (im : K → ℝ) := im_clm.continuous
+
+/-- Conjugate as a linear map -/
+noncomputable def conj_lm : K →ₗ[ℝ] K :=
+{ to_fun := λ x, conj x, map_add' := by simp, map_smul' := conj_smul, }
+
+@[simp] lemma conj_lm_coe : (conj_lm : K → K) = conj := rfl
+
+/-- Conjugate as a linear isometry -/
+noncomputable def conj_li : K →ₗᵢ[ℝ] K :=
+{ to_linear_map := conj_lm, norm_map' := by simp [norm_eq_abs] }
+
+@[simp] lemma conj_li_apply : (conj_li : K → K) = conj := rfl
+
+/-- Conjugate as a continuous linear map -/
+noncomputable def conj_clm : K →L[ℝ] K := conj_li.to_continuous_linear_map
+
+@[simp] lemma conj_clm_coe : ((conj_clm  : K →L[ℝ] K) : K →ₗ[ℝ] K) = conj_lm := rfl
+
+@[simp] lemma conj_clm_apply : (conj_clm : K → K) = conj := rfl
+
+@[simp] lemma conj_clm_norm : ∥(conj_clm : K →L[ℝ] K)∥ = 1 := conj_li.norm_to_continuous_linear_map
+
+@[continuity] lemma continuous_conj : continuous (conj : K → K) := conj_li.continuous
+
+/-- The `ℝ → K` coercion, as a linear map -/
+noncomputable def of_real_lm : ℝ →ₗ[ℝ] K :=
+{ to_fun := λ x, (x : K), map_add' := by simp, map_smul' := by simp, }
+
+@[simp] lemma of_real_lm_coe : (of_real_lm : ℝ → K) = coe := rfl
+
+/-- The ℝ → K coercion, as a linear isometry -/
+noncomputable def of_real_li : ℝ →ₗᵢ[ℝ] K :=
+{ to_linear_map := of_real_lm, norm_map' := by simp [norm_eq_abs] }
+
+@[simp] lemma of_real_li_apply : ((of_real_li : ℝ →ₗᵢ[ℝ] K) : ℝ → K) = coe := rfl
+
+/-- The `ℝ → K` coercion, as a continuous linear map -/
+noncomputable def of_real_clm : ℝ →L[ℝ] K := of_real_li.to_continuous_linear_map
+
+@[simp] lemma of_real_clm_coe : ((of_real_clm  : ℝ →L[ℝ] K) : ℝ →ₗ[ℝ] K) = of_real_lm := rfl
+
+@[simp] lemma of_real_clm_apply : (of_real_clm : ℝ → K) = coe := rfl
+
+@[simp] lemma of_real_clm_norm : ∥(of_real_clm : ℝ →L[ℝ] K)∥ = 1 :=
+of_real_li.norm_to_continuous_linear_map
+
+@[continuity] lemma continuous_of_real : continuous (coe : ℝ → K) := of_real_li.continuous
+
+end linear_maps
+
 end is_R_or_C
 
 section normalization