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

---
 Nevanlinna/complexHarmonic.lean | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index a27de54..828a180 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -1,4 +1,5 @@
 import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Complex.TaylorSeries
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.FDeriv.Basic
@@ -16,22 +17,36 @@ noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
 def Harmonic (f : ℂ → ℝ) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
+#check contDiff_iff_ftaylorSeries.2
 
-theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) : 
+lemma c2_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℂ 2 f := by
+  intro fHyp
+  exact Differentiable.contDiff fHyp
+
+lemma c2R_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℝ 2 f := by
+  intro fHyp
+  let ZZ := c2_if_holomorphic f fHyp
+  apply ContDiff.restrict_scalars ℝ ZZ
+
+
+
+theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
   Differentiable ℂ f → Harmonic (Complex.reCLM ∘ f) := by
 
   intro h
 
   constructor
-  · -- f is two times real continuously differentiable
-    sorry
+  · -- Complex.reCLM ∘ f is two times real continuously differentiable
+    apply ContDiff.comp
+    · -- Complex.reCLM is two times real continuously differentiable
+      exact ContinuousLinearMap.contDiff Complex.reCLM
+    · -- f is two times real continuously differentiable
+      exact c2R_if_holomorphic f h
 
   · -- Laplace of f is zero
     intro z
     unfold Complex.laplace
     simp
     let ZZ := (CauchyRiemann₃ (h z)).left
-    rw [ZZ]
-    
-    sorry
 
+    sorry