From 90d3aceb950bb2eabfbb84e13e73661018f28bd9 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 28 Apr 2024 21:09:38 +0200
Subject: [PATCH] cauchy riemann

---
 nevanlinna/cauchyRiemann.lean   | 50 +++++++++++++++++++++++++++++++++
 nevanlinna/complexHarmonic.lean |  0
 nevanlinna/realHarmonic.lean    | 16 +++++++----
 3 files changed, 61 insertions(+), 5 deletions(-)
 create mode 100644 nevanlinna/cauchyRiemann.lean
 create mode 100644 nevanlinna/complexHarmonic.lean

diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean
new file mode 100644
index 0000000..5d649ed
--- /dev/null
+++ b/nevanlinna/cauchyRiemann.lean
@@ -0,0 +1,50 @@
+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.FDeriv.Basic
+import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
+
+variable {z : ℂ} {f : ℂ → ℂ}
+
+example (h : DifferentiableAt ℂ f z) : f z = 0 := by
+
+  let A := fderiv ℂ f z
+  let B := fderiv ℝ f
+
+  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
+  let D := ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)
+  let E := D 1
+  let F := D Complex.I
+
+  have : A (Complex.I • 1) = Complex.I • (A 1) := by
+    exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1
+
+  let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
+  have : AR (Complex.I • 1) = Complex.I • (AR 1) := by
+    exact this
+
+  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
+  have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by
+    apply DifferentiableAt.lineDeriv_eq_fderiv
+    apply h.restrictScalars ℝ
+
+  have : D Complex.I = Complex.I * (D 1) := by
+    -- x
+
+    sorry
+
+  have : HasFDerivAt f A z := by
+    exact DifferentiableAt.hasFDerivAt h
+
+  have : HasFDerivAt f (B z) z := by
+    sorry
+
+
+  sorry
diff --git a/nevanlinna/complexHarmonic.lean b/nevanlinna/complexHarmonic.lean
new file mode 100644
index 0000000..e69de29
diff --git a/nevanlinna/realHarmonic.lean b/nevanlinna/realHarmonic.lean
index 6582dc0..b7889ae 100644
--- a/nevanlinna/realHarmonic.lean
+++ b/nevanlinna/realHarmonic.lean
@@ -1,10 +1,16 @@
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
 
-noncomputable def Real.laplace : (R [× n] → ℝ) → (ℂ → ℝ) := by
+noncomputable def Real.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
+  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₂₂
+
+structure Harmonic (f : ℝ × ℝ → ℝ) : Prop where
+  ker_Laplace : ∀ x, Real.laplace f x = 0
+  cont_Diff : ContDiff ℝ 2 f