From 4acac60a4f456ee017aecae86df4c858b1eab2df Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 14 May 2024 09:47:46 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 49 +++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 0ebc3fd..9961396 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -112,3 +112,52 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ
     rw [(holomorphic_is_harmonic h).right z]
     simp
     exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+
+
+theorem logabs_of_holomorphic_is_harmonic
+  {f : ℂ → ℂ}
+  (h₁ : Differentiable ℂ f)
+  (h₂ : ∀ z, f z ≠ 0) :
+  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 real C²
+  have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
+    unfold Complex.normSq
+    simp
+    apply ContDiff.add
+    apply ContDiff.mul
+    sorry
+
+  constructor
+  · -- logabs f is real C²
+
+    have : (fun z ↦ Real.log ‖f z‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by
+      funext z
+      simp
+      unfold Complex.abs
+      simp
+      rw [Real.log_sqrt]
+      exact Complex.normSq_nonneg (f z)
+    rw [this]
+    have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / 2) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
+      sorry
+    rw [this]
+
+    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
+
+  · -- Laplace vanishes
+    sorry