feat(analysis/complex): prove that complex functions are conformal if…

… and only if the functions are holomorphic/antiholomorphic with nonvanishing differential (#8424)

Complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential.


Co-authored-by: justadzr <66561890+justadzr@users.noreply.github.com>

src/analysis/calculus/conformal.lean

@@ -73,9 +73,7 @@ begin
       { exact ⟨(0 : X →L[ℝ] Y), has_fderiv_at_of_subsingleton f x,
         is_conformal_map_of_subsingleton 0⟩, },
       { exfalso,
-        rcases nontrivial_iff.mp w with ⟨a, b, hab⟩,
-        rw [fderiv_zero_of_not_differentiable_at h] at H,
-        exact hab (H.injective rfl), }, }, },
+        exact H.ne_zero (fderiv_zero_of_not_differentiable_at h), }, }, },
 end
 
 /-- A real differentiable map `f` is conformal at point `x` if and only if its
@@ -108,7 +106,7 @@ lemma comp {f : X → Y} {g : Y → Z} (x : X)
 begin
   rcases hf with ⟨f', hf₁, cf⟩,
   rcases hg with ⟨g', hg₁, cg⟩,
-  exact ⟨g'.comp f', hg₁.comp x hf₁, cf.comp cg⟩,
+  exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩,
 end
 
 lemma const_smul {f : X → Y} {x : X} {c : ℝ} (hc : c ≠ 0) (hf : conformal_at f x) :
@@ -134,13 +132,6 @@ lemma conformal_factor_at_inner_eq_mul_inner {f : E → F} {x : E} {f' : E →L[
   ⟪f' u, f' v⟫ = (conformal_factor_at H : ℝ) * ⟪u, v⟫ :=
 (H.differentiable_at.has_fderiv_at.unique h) ▸ conformal_factor_at_inner_eq_mul_inner' H u v
 
-/-- If a real differentiable map `f` is conformal at a point `x`,
-    then it preserves the angles at that point. -/
-lemma preserves_angle {f : E → F} {x : E} {f' : E →L[ℝ] F}
-  (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :
-  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
-let ⟨f₁, h₁, c⟩ := H in h₁.unique h ▸ c.preserves_angle u v
-
 end conformal_at
 
 end loc_conformality

src/analysis/complex/conformal.lean

@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2021 Yourong Zang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yourong Zang
+-/
+import analysis.complex.isometry
+import analysis.normed_space.conformal_linear_map
+
+/-!
+# Conformal maps between complex vector spaces
+
+We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces
+to be conformal.
+
+## Main results
+
+* `is_conformal_map_complex_linear`: a nonzero complex linear map into an arbitrary complex
+                                     normed space is conformal.
+* `is_conformal_map_complex_linear_conj`: the composition of a nonzero complex linear map with
+                                          `conj` is complex linear.
+* `is_conformal_map_iff_is_complex_or_conj_linear`: a real linear map between the complex
+                                                            plane is conformal iff it's complex
+                                                            linear or the composition of
+                                                            some complex linear map and `conj`.
+
+## Warning
+
+Antiholomorphic functions such as the complex conjugate are considered as conformal functions in
+this file.
+-/
+
+noncomputable theory
+
+open complex continuous_linear_map
+
+lemma is_conformal_map_conj : is_conformal_map (conj_lie : ℂ →L[ℝ] ℂ) :=
+conj_lie.to_linear_isometry.is_conformal_map
+
+section conformal_into_complex_normed
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
+  [is_scalar_tower ℝ ℂ E] {z : ℂ} {g : ℂ →L[ℝ] E} {f : ℂ → E}
+
+lemma is_conformal_map_complex_linear
+  {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) : is_conformal_map (map.restrict_scalars ℝ) :=
+begin
+  have minor₁ : ∥map 1∥ ≠ 0,
+  { simpa [ext_ring_iff] using nonzero },
+  refine ⟨∥map 1∥, minor₁, ⟨∥map 1∥⁻¹ • map, _⟩, _⟩,
+  { intros x,
+    simp only [linear_map.smul_apply],
+    have : x = x • 1 := by rw [smul_eq_mul, mul_one],
+    nth_rewrite 0 [this],
+    rw [_root_.coe_coe map, linear_map.coe_coe_is_scalar_tower],
+    simp only [map.coe_coe, map.map_smul, norm_smul, normed_field.norm_inv, norm_norm],
+    field_simp [minor₁], },
+  { ext1,
+    rw [← linear_isometry.coe_to_linear_map],
+    simp [minor₁], },
+end
+
+lemma is_conformal_map_complex_linear_conj
+  {map : ℂ →L[ℂ] E} (nonzero : map ≠ 0) :
+  is_conformal_map ((map.restrict_scalars ℝ).comp (conj_cle : ℂ →L[ℝ] ℂ)) :=
+(is_conformal_map_complex_linear nonzero).comp is_conformal_map_conj
+
+end conformal_into_complex_normed
+
+section conformal_into_complex_plane
+
+open continuous_linear_map
+
+variables {f : ℂ → ℂ} {z : ℂ} {g : ℂ →L[ℝ] ℂ}
+
+lemma is_conformal_map.is_complex_or_conj_linear (h : is_conformal_map g) :
+  (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g) ∨
+  (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g.comp ↑conj_cle) :=
+begin
+  rcases h with ⟨c, hc, li, hg⟩,
+  rcases linear_isometry_complex (li.to_linear_isometry_equiv rfl) with ⟨a, ha⟩,
+  let rot := c • (a : ℂ) • continuous_linear_map.id ℂ ℂ,
+  cases ha,
+  { refine or.intro_left _ ⟨rot, _⟩,
+    ext1,
+    simp only [coe_restrict_scalars', hg, ← li.coe_to_linear_isometry_equiv, ha,
+               pi.smul_apply, continuous_linear_map.smul_apply, rotation_apply,
+               continuous_linear_map.id_apply, smul_eq_mul], },
+  { refine or.intro_right _ ⟨rot, _⟩,
+    ext1,
+    rw [continuous_linear_map.coe_comp', hg, ← li.coe_to_linear_isometry_equiv, ha],
+    simp only [coe_restrict_scalars', function.comp_app, pi.smul_apply,
+               linear_isometry_equiv.coe_trans, conj_lie_apply,
+               rotation_apply, continuous_linear_equiv.coe_apply, conj_cle_apply],
+    simp only [continuous_linear_map.smul_apply, continuous_linear_map.id_apply,
+               smul_eq_mul, conj_conj], },
+end
+
+/-- A real continuous linear map on the complex plane is conformal if and only if the map or its
+    conjugate is complex linear, and the map is nonvanishing. -/
+lemma is_conformal_map_iff_is_complex_or_conj_linear:
+  is_conformal_map g ↔
+  ((∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g) ∨
+   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g.comp ↑conj_cle)) ∧ g ≠ 0 :=
+begin
+  split,
+  { exact λ h, ⟨h.is_complex_or_conj_linear, h.ne_zero⟩, },
+  { rintros ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩,
+    { refine is_conformal_map_complex_linear _,
+      contrapose! h₂ with w,
+      simp [w] },
+    { have minor₁ : g = (map.restrict_scalars ℝ).comp ↑conj_cle,
+      { ext1,
+        simp [hmap] },
+      rw minor₁ at ⊢ h₂,
+      refine is_conformal_map_complex_linear_conj _,
+      contrapose! h₂ with w,
+      simp [w] } }
+end
+
+end conformal_into_complex_plane

src/analysis/complex/real_deriv.lean

@@ -1,18 +1,36 @@
 /-
 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
+Authors: Sébastien Gouëzel, Yourong Zang
 -/
 import analysis.calculus.times_cont_diff
-import analysis.complex.basic
+import analysis.complex.conformal
+import analysis.calculus.conformal
 
 /-! # Real differentiability of complex-differentiable functions
 
 `has_deriv_at.real_of_complex` expresses that, if a function on `ℂ` is differentiable (over `ℂ`),
 then its restriction to `ℝ` is differentiable over `ℝ`, with derivative the real part of the
 complex derivative.
--/
 
+`differentiable_at.conformal_at` states that a real-differentiable function with a nonvanishing
+differential from the complex plane into an arbitrary complex-normed space is conformal at a point
+if it's holomorphic at that point. This is a version of Cauchy-Riemann equations.
+
+`conformal_at_iff_differentiable_at_or_differentiable_at_comp_conj` proves that a real-differential
+function with a nonvanishing differential between the complex plane is conformal at a point if and
+only if it's holomorphic or antiholomorphic at that point.
+
+## TODO
+
+* The classical form of Cauchy-Riemann equations
+* On a connected open set `u`, a function which is `conformal_at` each point is either holomorphic
+throughout or antiholomorphic throughout.
+
+## Warning
+
+We do NOT require conformal functions to be orientation-preserving in this file.
+-/
 
 section real_deriv_of_complex
 /-! ### Differentiability of the restriction to `ℝ` of complex functions -/
@@ -62,3 +80,47 @@ times_cont_diff_iff_times_cont_diff_at.2 $ λ x,
   h.times_cont_diff_at.real_of_complex
 
 end real_deriv_of_complex
+
+section conformality
+/-! ### Conformality of real-differentiable complex maps -/
+open complex continuous_linear_map
+
+variables
+
+/-- A real differentiable function of the complex plane into some complex normed space `E` is
+    conformal at a point `z` if it is holomorphic at that point with a nonvanishing differential.
+    This is a version of the Cauchy-Riemann equations. -/
+lemma differentiable_at.conformal_at {E : Type*}
+  [normed_group E] [normed_space ℝ E] [normed_space ℂ E]
+  [is_scalar_tower ℝ ℂ E] {z : ℂ} {f : ℂ → E}
+  (hf' : fderiv ℝ f z ≠ 0) (h : differentiable_at ℂ f z) :
+  conformal_at f z :=
+begin
+  rw conformal_at_iff_is_conformal_map_fderiv,
+  rw (h.has_fderiv_at.restrict_scalars ℝ).fderiv at ⊢ hf',
+  apply is_conformal_map_complex_linear,
+  contrapose! hf' with w,
+  simp [w]
+end
+
+/-- A complex function is conformal if and only if the function is holomorphic or antiholomorphic
+    with a nonvanishing differential. -/
+lemma conformal_at_iff_differentiable_at_or_differentiable_at_comp_conj {f : ℂ → ℂ} {z : ℂ} :
+  conformal_at f z ↔
+  (differentiable_at ℂ f z ∨ differentiable_at ℂ (f ∘ conj) (conj z)) ∧ fderiv ℝ f z ≠ 0 :=
+begin
+  rw conformal_at_iff_is_conformal_map_fderiv,
+  rw is_conformal_map_iff_is_complex_or_conj_linear,
+  apply and_congr_left,
+  intros h,
+  have h_diff := h.imp_symm fderiv_zero_of_not_differentiable_at,
+  apply or_congr,
+  { rw differentiable_at_iff_restrict_scalars ℝ h_diff },
+  rw ← conj_conj z at h_diff,
+  rw differentiable_at_iff_restrict_scalars ℝ (h_diff.comp _ conj_cle.differentiable_at),
+  refine exists_congr (λ g, rfl.congr _),
+  have : fderiv ℝ conj (conj z) = _ := conj_cle.fderiv,
+  simp [fderiv.comp _ h_diff conj_cle.differentiable_at, this, conj_conj],
+end
+
+end conformality

src/analysis/normed_space/conformal_linear_map.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Yourong Zang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 -/
-import geometry.euclidean.basic
 import analysis.normed_space.inner_product
 
 /-!
@@ -59,6 +58,10 @@ lemma is_conformal_map_id : is_conformal_map (id R M) :=
 lemma is_conformal_map_const_smul {c : R} (hc : c ≠ 0) : is_conformal_map (c • (id R M)) :=
 ⟨c, hc, id, by ext; simp⟩
 
+lemma linear_isometry.is_conformal_map (f' : E →ₗᵢ[ℝ] F) :
+  is_conformal_map f'.to_continuous_linear_map :=
+⟨1, one_ne_zero, f', by ext; simp⟩
+
 lemma is_conformal_map_iff (f' : E →L[ℝ] F) :
   is_conformal_map f' ↔ ∃ (c : ℝ), 0 < c ∧
   ∀ (u v : E), ⟪f' u, f' v⟫ = (c : ℝ) * ⟪u, v⟫ :=
@@ -98,7 +101,7 @@ end
 namespace is_conformal_map
 
 lemma comp {f' : M →L[R] N} {g' : N →L[R] G}
-  (hf' : is_conformal_map f') (hg' : is_conformal_map g') :
+  (hg' : is_conformal_map g') (hf' : is_conformal_map f') :
   is_conformal_map (g'.comp f') :=
 begin
   rcases hf' with ⟨cf, hcf, lif, hlif⟩,
@@ -112,20 +115,14 @@ lemma injective {f' : M →L[R] N} (h : is_conformal_map f') : function.injectiv
 let ⟨c, hc, li, hf'⟩ := h in by simp only [hf', pi.smul_def];
   exact (smul_left_injective _ hc).comp li.injective
 
-lemma preserves_angle {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
-  inner_product_geometry.angle (f' u) (f' v) = inner_product_geometry.angle u v :=
+lemma ne_zero [nontrivial M] {f' : M →L[R] N} (hf' : is_conformal_map f') :
+  f' ≠ 0 :=
 begin
-  obtain ⟨c, hc, li, hcf⟩ := h,
-  suffices : c * (c * inner u v) / (∥c∥ * ∥u∥ * (∥c∥ * ∥v∥)) = inner u v / (∥u∥ * ∥v∥),
-  { simp [this, inner_product_geometry.angle, hcf, norm_smul, inner_smul_left, inner_smul_right] },
-  by_cases hu : ∥u∥ = 0,
-  { simp [norm_eq_zero.mp hu] },
-  by_cases hv : ∥v∥ = 0,
-  { simp [norm_eq_zero.mp hv] },
-  have hc : ∥c∥ ≠ 0 := λ w, hc (norm_eq_zero.mp w),
-  field_simp,
-  have : c * c = ∥c∥ * ∥c∥ := by simp [real.norm_eq_abs, abs_mul_abs_self],
-  convert congr_arg (λ x, x * ⟪u, v⟫ * ∥u∥ * ∥v∥) this using 1; ring,
+  intros w,
+  rcases exists_ne (0 : M) with ⟨a, ha⟩,
+  have : f' a = f' 0,
+  { simp_rw [w, continuous_linear_map.zero_apply], },
+  exact ha (hf'.injective this),
 end
 
 end is_conformal_map

src/geometry/euclidean/basic.lean

@@ -3,13 +3,13 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Manuel Candales
 -/
-import analysis.normed_space.inner_product
 import analysis.special_functions.trigonometric
 import algebra.quadratic_discriminant
 import analysis.normed_space.add_torsor
 import data.matrix.notation
 import linear_algebra.affine_space.finite_dimensional
 import tactic.fin_cases
+import analysis.calculus.conformal
 
 /-!
 # Euclidean spaces
@@ -75,6 +75,33 @@ variables {V : Type*} [inner_product_space ℝ V]
 this is π/2. -/
 def angle (x y : V) : ℝ := real.arccos (inner x y / (∥x∥ * ∥y∥))
 
+lemma is_conformal_map.preserves_angle {E F : Type*}
+  [inner_product_space ℝ E] [inner_product_space ℝ F]
+  {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
+  angle (f' u) (f' v) = angle u v :=
+begin
+  obtain ⟨c, hc, li, hcf⟩ := h,
+  suffices : c * (c * inner u v) / (∥c∥ * ∥u∥ * (∥c∥ * ∥v∥)) = inner u v / (∥u∥ * ∥v∥),
+  { simp [this, angle, hcf, norm_smul, inner_smul_left, inner_smul_right] },
+  by_cases hu : ∥u∥ = 0,
+  { simp [norm_eq_zero.mp hu] },
+  by_cases hv : ∥v∥ = 0,
+  { simp [norm_eq_zero.mp hv] },
+  have hc : ∥c∥ ≠ 0 := λ w, hc (norm_eq_zero.mp w),
+  field_simp,
+  have : c * c = ∥c∥ * ∥c∥ := by simp [real.norm_eq_abs, abs_mul_abs_self],
+  convert congr_arg (λ x, x * ⟪u, v⟫ * ∥u∥ * ∥v∥) this using 1; ring,
+end
+
+/-- If a real differentiable map `f` is conformal at a point `x`,
+    then it preserves the angles at that point. -/
+lemma conformal_at.preserves_angle {E F : Type*}
+  [inner_product_space ℝ E] [inner_product_space ℝ F]
+  {f : E → F} {x : E} {f' : E →L[ℝ] F}
+  (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :
+  angle (f' u) (f' v) = angle u v :=
+let ⟨f₁, h₁, c⟩ := H in h₁.unique h ▸ is_conformal_map.preserves_angle c u v
+
 /-- The cosine of the angle between two vectors. -/
 lemma cos_angle (x y : V) : real.cos (angle x y) = inner x y / (∥x∥ * ∥y∥) :=
 real.cos_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1