Split off file

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

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