From 710de9372baea90bb2a2175b6791d34139ac3333 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 16 May 2024 10:01:15 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 79 ++++++++++++++-------------------
 1 file changed, 34 insertions(+), 45 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index e2944b0..0f19833 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -122,28 +122,7 @@ theorem logabs_of_holomorphic_is_harmonic
   (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₁)
-
-  -- Complex.log ∘ f is real C²
-  have t₀ : Differentiable ℂ (Complex.log ∘ f) := by
-    intro z
-    apply DifferentiableAt.comp
-    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'
+  /- We start with a number of lemmas on regularity of all the functions involved -/
 
   -- The norm square is real C²
   have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
@@ -161,6 +140,18 @@ theorem logabs_of_holomorphic_is_harmonic
     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
@@ -171,6 +162,19 @@ theorem logabs_of_holomorphic_is_harmonic
     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
+    unfold Function.comp
+    rw [Complex.log_conj]
+    rfl
+    exact Complex.slitPlane_arg_ne_pi (h₃ z)
+
+
+
+
   constructor
   · -- logabs f is real C²
     have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
@@ -190,15 +194,8 @@ theorem logabs_of_holomorphic_is_harmonic
 
     apply contDiff_iff_contDiffAt.2
     intro z
-
     apply ContDiffAt.const_smul
-    apply ContDiffAt.comp
-    apply Real.contDiffAt_log.2
-    simp
-    exact h₂ z
-    apply ContDiffAt.comp
-    exact ContDiff.contDiffAt normSq_is_real_C2
-    exact ContDiff.contDiffAt f_is_real_C2
+    exact ContDiff.contDiffAt t₄
 
   · -- Laplace vanishes
     have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
@@ -258,31 +255,23 @@ theorem logabs_of_holomorphic_is_harmonic
     rw [this]
     rw [laplace_add]
 
-    have t₁: Complex.laplace (Complex.log ∘ f) = 0 := by
-      let A := holomorphic_is_harmonic t₀
-      funext z
-      exact A.2 z
-    rw [t₁]
+    rw [t₂, laplace_compCLE]
+    intro z
     simp
-
-    rw [t₂]
-
-    rw [t₃]
-    rw [laplace_compCLE]
-    rw [t₁]
+    rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z]
     simp
 
     -- ContDiff ℝ 2 (Complex.log ∘ f)
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
 
     -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f)
-    rw [t₂, t₃]
+    rw [t₂]
     apply ContDiff.comp
     exact ContinuousLinearEquiv.contDiff Complex.conjCLE
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
 
     -- ContDiff ℝ 2 (Complex.log ∘ f)
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀)
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic)
 
     -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f)
     exact t₄