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

---
 Nevanlinna/complexHarmonic.lean | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 7cfa999..0ebc3fd 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -85,5 +85,30 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
 theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
   Harmonic (Complex.reCLM ∘ f) := by
 
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.reCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-  sorry
+
+theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
+  Harmonic (Complex.imCLM ∘ f) := by
+
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.imCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)