From 058ea29a6494a7c67dd4c718d249058f9e69dc66 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 15 May 2024 10:09:22 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 63 +++++++++++++++++++++++++++++++--
 1 file changed, 61 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index da7ec8b..94ad6d6 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -117,13 +117,17 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ
 theorem logabs_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0) :
+  (h₂ : ∀ z, f z ≠ 0)
+  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
   Harmonic (fun z ↦ Real.log ‖f z‖) := by
 
   -- f is real C²
   have f_is_real_C2 : ContDiff ℝ 2 f :=
     ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁)
 
+  -- The norm square is z * z.conj
+  have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
+
   -- The norm square is real C²
   have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
     unfold Complex.normSq
@@ -149,7 +153,7 @@ theorem logabs_of_holomorphic_is_harmonic
       simp
       rw [Real.log_sqrt]
       rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
-      exact Complex.normSq_nonneg (f z)  
+      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
@@ -169,5 +173,60 @@ theorem logabs_of_holomorphic_is_harmonic
     exact ContDiff.contDiffAt f_is_real_C2
 
   · -- 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
+      sorry
+    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]
 
     sorry
+    sorry