From f85fafd05f7178fad20e1957284bbf231dd7c49b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Apr 2024 08:20:57 +0200
Subject: [PATCH] Working...

---
 Nevanlinna.lean                               |  2 +-
 {nevanlinna => Nevanlinna}/cauchyRiemann.lean |  0
 Nevanlinna/complexHarmonic.lean               | 37 ++++++++++++++++++
 {nevanlinna => Nevanlinna}/harmonic.lean      |  0
 {nevanlinna => Nevanlinna}/logabs.lean        |  0
 {nevanlinna => Nevanlinna}/realHarmonic.lean  |  0
 {nevanlinna => Nevanlinna}/test.lean          |  0
 nevanlinna/complexHarmonic.lean               | 39 -------------------
 8 files changed, 38 insertions(+), 40 deletions(-)
 rename {nevanlinna => Nevanlinna}/cauchyRiemann.lean (100%)
 create mode 100644 Nevanlinna/complexHarmonic.lean
 rename {nevanlinna => Nevanlinna}/harmonic.lean (100%)
 rename {nevanlinna => Nevanlinna}/logabs.lean (100%)
 rename {nevanlinna => Nevanlinna}/realHarmonic.lean (100%)
 rename {nevanlinna => Nevanlinna}/test.lean (100%)
 delete mode 100644 nevanlinna/complexHarmonic.lean

diff --git a/Nevanlinna.lean b/Nevanlinna.lean
index e99d3a6..eba18bb 100644
--- a/Nevanlinna.lean
+++ b/Nevanlinna.lean
@@ -1 +1 @@
-def hello := "world"
\ No newline at end of file
+import Nevanlinna.cauchyRiemann
\ No newline at end of file
diff --git a/nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean
similarity index 100%
rename from nevanlinna/cauchyRiemann.lean
rename to Nevanlinna/cauchyRiemann.lean
diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
new file mode 100644
index 0000000..a27de54
--- /dev/null
+++ b/Nevanlinna/complexHarmonic.lean
@@ -0,0 +1,37 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+import Nevanlinna.cauchyRiemann
+
+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₂₂
+
+
+def Harmonic (f : ℂ → ℝ) : Prop :=
+  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
+
+
+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
+
+  · -- Laplace of f is zero
+    intro z
+    unfold Complex.laplace
+    simp
+    let ZZ := (CauchyRiemann₃ (h z)).left
+    rw [ZZ]
+    
+    sorry
+
diff --git a/nevanlinna/harmonic.lean b/Nevanlinna/harmonic.lean
similarity index 100%
rename from nevanlinna/harmonic.lean
rename to Nevanlinna/harmonic.lean
diff --git a/nevanlinna/logabs.lean b/Nevanlinna/logabs.lean
similarity index 100%
rename from nevanlinna/logabs.lean
rename to Nevanlinna/logabs.lean
diff --git a/nevanlinna/realHarmonic.lean b/Nevanlinna/realHarmonic.lean
similarity index 100%
rename from nevanlinna/realHarmonic.lean
rename to Nevanlinna/realHarmonic.lean
diff --git a/nevanlinna/test.lean b/Nevanlinna/test.lean
similarity index 100%
rename from nevanlinna/test.lean
rename to Nevanlinna/test.lean
diff --git a/nevanlinna/complexHarmonic.lean b/nevanlinna/complexHarmonic.lean
deleted file mode 100644
index 4318c6d..0000000
--- a/nevanlinna/complexHarmonic.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-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