From 015ab141311c1708588da91a349189434fe79413 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 16 May 2024 09:37:17 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 48 +++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 20 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 7be3c94..e2944b0 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -133,6 +133,15 @@ theorem logabs_of_holomorphic_is_harmonic
     exact Complex.differentiableAt_log (h₃ z)
     exact h₁ z
 
+  have t₂ : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
+    funext z
+    unfold Function.comp
+    rw [Complex.log_conj]
+    exact Complex.slitPlane_arg_ne_pi (h₃ z)
+
+  have t₃ : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
+    rfl
+
   -- The norm square is z * z.conj
   have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'
 
@@ -152,6 +161,16 @@ theorem logabs_of_holomorphic_is_harmonic
     apply ContinuousLinearMap.contDiff Complex.imCLM
     apply ContinuousLinearMap.contDiff Complex.imCLM
 
+  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
+
   constructor
   · -- logabs f is real C²
     have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
@@ -198,7 +217,8 @@ theorem logabs_of_holomorphic_is_harmonic
       intro z
       rw [laplace_compContLin]
       simp
-      sorry
+      -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
+      exact t₄
     conv =>
       intro z
       rw [this z]
@@ -245,16 +265,9 @@ theorem logabs_of_holomorphic_is_harmonic
     rw [t₁]
     simp
 
-    have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
-      funext z
-      unfold Function.comp
-      rw [Complex.log_conj]
-      exact Complex.slitPlane_arg_ne_pi (h₃ z)
-    rw [this]
+    rw [t₂]
 
-    have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-      rfl
-    rw [this]
+    rw [t₃]
     rw [laplace_compCLE]
     rw [t₁]
     simp
@@ -263,18 +276,13 @@ theorem logabs_of_holomorphic_is_harmonic
     exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
 
     -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
-
-    sorry
+    rw [t₂, t₃]
+    apply ContDiff.comp
+    exact ContinuousLinearEquiv.contDiff Complex.conjCLE
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
 
     -- ContDiff ℝ 2 (Complex.log ∘ f)
     exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
 
     -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
-    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
+    exact t₄