From d5f34a31101198b8b5928fe98e24ac74419dbd30 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 13 May 2024 09:23:08 +0200
Subject: [PATCH] Split off file

---
 Nevanlinna/complexHarmonic.lean | 19 ++++++++++---------
 Nevanlinna/laplace.lean         | 25 +++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 9 deletions(-)
 create mode 100644 Nevanlinna/laplace.lean

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 8c19276..7cfa999 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -12,19 +12,13 @@ import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Topology.Instances.RealVectorSpace
 import Nevanlinna.cauchyRiemann
+import Nevanlinna.laplace
 import Nevanlinna.partialDeriv
 
-
-noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
-  intro f
-  let fx  := partialDeriv ℝ 1 f
-  let fxx := partialDeriv ℝ 1 fx
-  let fy  := partialDeriv ℝ Complex.I f
-  let fyy := partialDeriv ℝ Complex.I fy
-  exact fxx + fyy
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 
-def Harmonic (f : ℂ → ℂ) : Prop :=
+def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
@@ -86,3 +80,10 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
     exact fI_is_real_differentiable
     -- Differentiable ℝ (Real.partialDeriv 1 f)
     exact fI_is_real_differentiable
+
+
+theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
+  Harmonic (Complex.reCLM ∘ f) := by
+
+
+  sorry
diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
new file mode 100644
index 0000000..49d35bf
--- /dev/null
+++ b/Nevanlinna/laplace.lean
@@ -0,0 +1,25 @@
+import Mathlib.Data.Fin.Tuple.Basic
+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
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+import Mathlib.Data.Complex.Module
+import Mathlib.Data.Complex.Order
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Topology.Algebra.InfiniteSum.Module
+import Mathlib.Topology.Instances.RealVectorSpace
+import Nevanlinna.cauchyRiemann
+import Nevanlinna.partialDeriv
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) := by
+  intro f
+  let fx  := partialDeriv ℝ 1 f
+  let fxx := partialDeriv ℝ 1 fx
+  let fy  := partialDeriv ℝ Complex.I f
+  let fyy := partialDeriv ℝ Complex.I fy
+  exact fxx + fyy