From ef75cb4579dff34e72a3b69458e95bed84e12d12 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 28 Apr 2024 21:17:45 +0200
Subject: [PATCH] working...

---
 nevanlinna/cauchyRiemann.lean   | 17 +++++++-------
 nevanlinna/complexHarmonic.lean | 39 +++++++++++++++++++++++++++++++++
 nevanlinna/realHarmonic.lean    |  6 ++---
 3 files changed, 50 insertions(+), 12 deletions(-)

diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean
index 5d649ed..db56f16 100644
--- a/nevanlinna/cauchyRiemann.lean
+++ b/nevanlinna/cauchyRiemann.lean
@@ -1,15 +1,14 @@
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-import Mathlib.Analysis.Complex.RealDeriv
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.Calculus.Deriv.Linear
-import Mathlib.Analysis.Complex.Conformal
 import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.Deriv.Linear
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Complex.CauchyIntegral
+import Mathlib.Analysis.Complex.Conformal
+import Mathlib.Analysis.Complex.RealDeriv
 
 variable {z : ℂ} {f : ℂ → ℂ}
 
diff --git a/nevanlinna/complexHarmonic.lean b/nevanlinna/complexHarmonic.lean
index e69de29..4318c6d 100644
--- a/nevanlinna/complexHarmonic.lean
+++ b/nevanlinna/complexHarmonic.lean
@@ -0,0 +1,39 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+
+noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) := by
+  intro f
+  let f₁ := fun x ↦ lineDeriv ℝ f x ⟨1,0⟩
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x ⟨1,0⟩
+  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x ⟨0,1⟩
+  exact f₁₁ + f₂₂
+
+noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
+  intro f
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
+  exact f₁₁ + f₂₂
+
+
+theorem xx : ∀ f : ℂ → , f = 0  := by
+  intro f
+
+  let f₁ := fun x ↦ lineDeriv ℝ f x 1
+  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
+
+  have : ∀ z, fderiv ℂ f z = 0 := by
+    sorry
+
+
+  have : (fun x ↦ lineDeriv ℝ f x 1) = (fun x ↦ lineDeriv ℝ f x Complex.I) := by
+
+    unfold lineDeriv
+
+    sorry
+
+  sorry
diff --git a/nevanlinna/realHarmonic.lean b/nevanlinna/realHarmonic.lean
index b7889ae..92db0ab 100644
--- a/nevanlinna/realHarmonic.lean
+++ b/nevanlinna/realHarmonic.lean
@@ -11,6 +11,6 @@ noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) :
 
   exact f₁₁ + f₂₂
 
-structure Harmonic (f : ℝ × ℝ → ℝ) : Prop where
-  ker_Laplace : ∀ x, Real.laplace f x = 0
-  cont_Diff : ContDiff ℝ 2 f
+
+def Harmonic (f : ℝ × ℝ → ℝ) : Prop :=
+  (ContDiff ℝ 2 f) ∧ (∀ x, Real.laplace f x = 0)