Nevanlinna/cauchyRiemann.lean

@@ -44,7 +44,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
   simp
 
 
-theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f)
+theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
   → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
   unfold partialDeriv

Nevanlinna/complexHarmonic.lean

@@ -26,50 +26,20 @@ def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
-theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
+theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}  (h : Harmonic f) :
-  Harmonic (f₁ + f₂) := by
-  constructor
-  · exact ContDiff.add h₁.1 h₂.1
-  · rw [laplace_add h₁.1 h₂.1]
-    simp
-    intro z
-    rw [h₁.2 z, h₂.2 z]
-    simp
-
-
-theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) :
-  Harmonic (c • f) := by
-  constructor
-  · exact ContDiff.const_smul c h.1
-  · rw [laplace_smul h.1]
-    dsimp
-    intro z
-    rw [h.2 z]
-    simp
-
-
-theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) :
-  Harmonic f ↔ Harmonic (c • f) := by
-  constructor
-  · exact harmonic_smul_const_is_harmonic
-  · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
-    exact fun a => harmonic_smul_const_is_harmonic a
-
-
-theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
   Harmonic (l ∘ f) := by
 
   constructor
   · -- Continuous differentiability
     apply ContDiff.comp
     exact ContinuousLinearMap.contDiff l
-    exact h.1
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
   · rw [laplace_compContLin]
     simp
     intro z
     rw [h.2 z]
     simp
-    exact ContDiff.restrict_scalars ℝ h.1
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
 
 theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@@ -79,7 +49,7 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
   · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
     rw [this]
     exact harmonic_comp_CLM_is_harmonic
-  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
+  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by 
       funext z
       unfold Function.comp
       simp
@@ -108,17 +78,21 @@ theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
     -- This lemma says that partial derivatives commute with complex scalar
     -- multiplication. This is a consequence of partialDeriv_compContLin once we
     -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
+    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
       intro v s g hg
 
       -- Present scalar multiplication as a continuous ℝ-linear map. This is
       -- horrible, there must be better ways to do that.
-      let sMuls : F₁ →L[ℝ] F₁ :=
+      let sMuls : ℂ →L[ℝ] ℂ :=
       {
-        toFun := fun x ↦ s • x
+        toFun := fun x ↦ s * x
-        map_add' := by exact fun x y => DistribSMul.smul_add s x y
+        map_add' := by
-        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
+          intro x y
-        cont := continuous_const_smul s
+          ring
+        map_smul' := by
+          intro m x
+          simp
+          ring
       }
 
       -- Bring the goal into a form that is recognized by
@@ -155,12 +129,6 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ
   exact holomorphic_is_harmonic h
 
 
-theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.conjCLE ∘ f) := by
-  apply harmonic_iff_comp_CLE_is_harmonic.1
-  exact holomorphic_is_harmonic h
-
-
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)
@@ -168,58 +136,151 @@ theorem log_normSq_of_holomorphic_is_harmonic
   (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
   Harmonic (Real.log ∘ Complex.normSq ∘ f) := by
 
-  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
-
-  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
-    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
-      funext z
-      simp
-      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
-      rw [Complex.normSq_eq_conj_mul_self]
-    rw [this]
-    exact hyp
 
 
-  -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
+  /- We start with a number of lemmas on regularity of all the functions involved -/
-  -- THIS IS WHERE WE USE h₃
+
-  have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
+  -- The norm square is real C²
-    unfold Function.comp
+  have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
-    funext z
+    unfold Complex.normSq
     simp
-    rw [Complex.log_mul_eq_add_log_iff]
+    conv =>
+      arg 3
+      intro x
+      rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
+    apply ContDiff.add
+    apply ContDiff.mul
+    apply ContinuousLinearMap.contDiff Complex.reCLM
+    apply ContinuousLinearMap.contDiff Complex.reCLM
+    apply ContDiff.mul
+    apply ContinuousLinearMap.contDiff Complex.imCLM
+    apply ContinuousLinearMap.contDiff Complex.imCLM
 
-    have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
+  -- f is real C²
-      rw [Complex.arg_conj]
+  have f_is_real_C2 : ContDiff ℝ 2 f :=
-      have : ¬ Complex.arg (f z) = Real.pi := by
+    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
-        exact Complex.slitPlane_arg_ne_pi (h₃ z)
+
-      simp
+  -- Complex.log ∘ f is real C²
-      tauto
+  have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
-    rw [this]
+    intro z
+    apply DifferentiableAt.comp
+    exact Complex.differentiableAt_log (h₃ z)
+    exact h₁ z
+
+  -- Real.log |f|² is real C²
+  have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
+    rw [contDiff_iff_contDiffAt]
+    intro z
+    apply ContDiffAt.comp
+    apply Real.contDiffAt_log.mpr
     simp
-    constructor
-    · exact Real.pi_pos
-    · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
     exact h₂ z
-  rw [this]
+    apply ContDiff.comp_contDiffAt z normSq_is_real_C2
+    exact ContDiff.contDiffAt f_is_real_C2
 
-  apply harmonic_add_harmonic_is_harmonic
+  have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
     funext z
     unfold Function.comp
     rw [Complex.log_conj]
     rfl
     exact Complex.slitPlane_arg_ne_pi (h₃ z)
-  rw [this]
-  rw [← harmonic_iff_comp_CLE_is_harmonic]
 
-  repeat
+  constructor
-    apply holomorphic_is_harmonic
+  · -- logabs f is real C²
+    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+      funext z
+      simp
+      unfold Complex.abs
+      simp
+      rw [Real.log_sqrt]
+      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+
+    have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
+      exact rfl
+    rw [this]
+    apply ContDiff.const_smul
+    exact t₄
+
+  · -- Laplace vanishes
+    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+      funext z
+      simp
+      unfold Complex.abs
+      simp
+      rw [Real.log_sqrt]
+      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+    rw [laplace_smul]
+    simp
+
+    have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
+      intro z
+      rw [laplace_compContLin]
+      simp
+      -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+      exact t₄
+    conv =>
+      intro z
+      rw [this z]
+
+    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
+      unfold Function.comp
+      funext z
+      apply Complex.ofReal_log
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+
+    have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
+      funext z
+      simp
+      exact Complex.normSq_eq_conj_mul_self
+    rw [this]
+
+    have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
+      unfold Function.comp
+      funext z
+      simp
+      rw [Complex.log_mul_eq_add_log_iff]
+
+      have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
+        rw [Complex.arg_conj]
+        have : ¬ Complex.arg (f z) = Real.pi := by
+          exact Complex.slitPlane_arg_ne_pi (h₃ z)
+        simp
+        tauto
+      rw [this]
+      simp
+      constructor
+      · exact Real.pi_pos
+      · exact Real.pi_nonneg
+      exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
+      exact h₂ z
+    rw [this]
+    rw [laplace_add]
+
+    rw [t₂, laplace_compCLE]
     intro z
-    apply DifferentiableAt.comp
+    simp
-    exact Complex.differentiableAt_log (h₃ z)
+    rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
-    exact h₁ z
+    simp
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
+    rw [t₂]
+    apply ContDiff.comp
+    exact ContinuousLinearEquiv.contDiff Complex.conjCLE
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+    exact t₄
 
 
 theorem logabs_of_holomorphic_is_harmonic
@@ -229,18 +290,146 @@ theorem logabs_of_holomorphic_is_harmonic
   (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
   Harmonic (fun z ↦ Real.log ‖f z‖) := by
 
-  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
+  /- We start with a number of lemmas on regularity of all the functions involved -/
-  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+
+  -- The norm square is real C²
+  have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
+    unfold Complex.normSq
+    simp
+    conv =>
+      arg 3
+      intro x
+      rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
+    apply ContDiff.add
+    apply ContDiff.mul
+    apply ContinuousLinearMap.contDiff Complex.reCLM
+    apply ContinuousLinearMap.contDiff Complex.reCLM
+    apply ContDiff.mul
+    apply ContinuousLinearMap.contDiff Complex.imCLM
+    apply ContinuousLinearMap.contDiff Complex.imCLM
+
+  -- f is real C²
+  have f_is_real_C2 : ContDiff ℝ 2 f :=
+    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
+
+  -- Complex.log ∘ f is real C²
+  have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by
+    intro z
+    apply DifferentiableAt.comp
+    exact Complex.differentiableAt_log (h₃ z)
+    exact h₁ z
+
+  -- Real.log |f|² is real C²
+  have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by
+    rw [contDiff_iff_contDiffAt]
+    intro z
+    apply ContDiffAt.comp
+    apply Real.contDiffAt_log.mpr
+    simp
+    exact h₂ z
+    apply ContDiff.comp_contDiffAt z normSq_is_real_C2
+    exact ContDiff.contDiffAt f_is_real_C2
+
+  have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
     funext z
-    simp
+    unfold Function.comp
-    unfold Complex.abs
+    rw [Complex.log_conj]
-    simp
+    rfl
-    rw [Real.log_sqrt]
+    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
-    exact Complex.normSq_nonneg (f z)
-  rw [this]
 
-  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
+  constructor
-  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
+  · -- logabs f is real C²
+    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+      funext z
+      simp
+      unfold Complex.abs
+      simp
+      rw [Real.log_sqrt]
+      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
 
-  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃
+    have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
+      exact rfl
+    rw [this]
+    apply ContDiff.const_smul
+    exact t₄
+
+  · -- Laplace vanishes
+    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+      funext z
+      simp
+      unfold Complex.abs
+      simp
+      rw [Real.log_sqrt]
+      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+    rw [laplace_smul]
+    simp
+
+    have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
+      intro z
+      rw [laplace_compContLin]
+      simp
+      -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+      exact t₄
+    conv =>
+      intro z
+      rw [this z]
+
+    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
+      unfold Function.comp
+      funext z
+      apply Complex.ofReal_log
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+
+    have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
+      funext z
+      simp
+      exact Complex.normSq_eq_conj_mul_self
+    rw [this]
+
+    have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
+      unfold Function.comp
+      funext z
+      simp
+      rw [Complex.log_mul_eq_add_log_iff]
+
+      have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
+        rw [Complex.arg_conj]
+        have : ¬ Complex.arg (f z) = Real.pi := by
+          exact Complex.slitPlane_arg_ne_pi (h₃ z)
+        simp
+        tauto
+      rw [this]
+      simp
+      constructor
+      · exact Real.pi_pos
+      · exact Real.pi_nonneg
+      exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
+      exact h₂ z
+    rw [this]
+    rw [laplace_add]
+
+    rw [t₂, laplace_compCLE]
+    intro z
+    simp
+    rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
+    simp
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
+    rw [t₂]
+    apply ContDiff.comp
+    exact ContinuousLinearEquiv.contDiff Complex.conjCLE
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Complex.log ∘ f)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
+
+    -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+    exact t₄