feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436)

Complex conjugation is a linear isometry (and various corollaries, eg it is a continuous linear map).

Also rewrite the results that `re` and `im` are continuous linear maps, to deduce from explicit bounds rather than passing through `linear_map.continuous_of_finite_dimensional`.

Author: hrmacbeth

src/analysis/complex/basic.lean

@@ -3,7 +3,6 @@ Copyright (c) Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.normed_space.finite_dimension
 import data.complex.module
 import data.complex.is_R_or_C
 
@@ -80,7 +79,8 @@ instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.re : ℂ →L[ℝ] ℝ := linear_map.re.to_continuous_linear_map
+def continuous_linear_map.re : ℂ →L[ℝ] ℝ :=
+linear_map.re.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
 
@@ -92,12 +92,13 @@ def continuous_linear_map.re : ℂ →L[ℝ] ℝ := linear_map.re.to_continuous_
 
 @[simp] lemma continuous_linear_map.re_norm :
   ∥continuous_linear_map.re∥ = 1 :=
-le_antisymm (op_norm_le_bound _ zero_le_one $ λ z, by simp [real.norm_eq_abs, abs_re_le_abs]) $
+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)
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.im : ℂ →L[ℝ] ℝ := linear_map.im.to_continuous_linear_map
+def continuous_linear_map.im : ℂ →L[ℝ] ℝ :=
+linear_map.im.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
 
@@ -109,10 +110,30 @@ def continuous_linear_map.im : ℂ →L[ℝ] ℝ := linear_map.im.to_continuous_
 
 @[simp] lemma continuous_linear_map.im_norm :
   ∥continuous_linear_map.im∥ = 1 :=
-le_antisymm (op_norm_le_bound _ zero_le_one $ λ z, by simp [real.norm_eq_abs, abs_im_le_abs]) $
+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)
 
+/-- The complex-conjugation function from `ℂ` to itself is an isometric linear map. -/
+def linear_isometry.conj : ℂ →ₗᵢ[ℝ] ℂ := ⟨linear_map.conj, λ 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
+
+lemma isometry_conj : isometry (conj : ℂ → ℂ) := linear_isometry.conj.isometry
+
+@[continuity] lemma continuous_conj : continuous conj := continuous_linear_map.conj.continuous
+
+@[simp] lemma continuous_linear_map.conj_coe :
+  (coe (continuous_linear_map.conj) : ℂ →ₗ[ℝ] ℂ) = linear_map.conj := rfl
+
+@[simp] lemma continuous_linear_map.conj_apply (z : ℂ) :
+  (continuous_linear_map.conj : ℂ → ℂ) z = z.conj := rfl
+
+@[simp] lemma continuous_linear_map.conj_norm :
+  ∥continuous_linear_map.conj∥ = 1 :=
+linear_isometry.conj.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⟩
 

src/data/complex/module.lean

@@ -145,4 +145,11 @@ def linear_map.of_real : ℝ →ₗ[ℝ] ℂ :=
 
 @[simp] lemma linear_map.coe_of_real : ⇑linear_map.of_real = coe := rfl
 
+/-- `ℝ`-linear map version of the complex conjugation function from `ℂ` to `ℂ`. -/
+def linear_map.conj : ℂ →ₗ[ℝ] ℂ :=
+{ map_smul' := by simp [restrict_scalars_smul_def],
+  ..conj }
+
+@[simp] lemma linear_map.coe_conj : ⇑linear_map.conj = conj := rfl
+
 end complex