From a1910c3a728e0f9174701eab6bfc13edb6b1109c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 7 May 2024 10:16:23 +0200
Subject: [PATCH] Working...

---
 Nevanlinna/complexHarmonic.lean | 54 +++------------------------------
 Nevanlinna/partialDeriv.lean    | 49 ++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 49 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index d3287bc..587016b 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -71,7 +71,6 @@ lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
   · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
   · simp
 
-#check partialDeriv_contDiff
 
 theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   Harmonic f := by
@@ -80,62 +79,19 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   have f_is_real_C2 : ContDiff ℝ 2 f :=
     ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-  -- f is real differentiable
-  have f_is_real_differentiable : Differentiable ℝ f := by
-    exact (contDiff_succ_iff_fderiv.1 f_is_real_C2).left
-
   have fI_is_real_differentiable : Differentiable ℝ (Real.partialDeriv 1 f) := by
-    let A := partialDeriv_contDiff f_is_real_C2 1
-    exact (contDiff_succ_iff_fderiv.1 A).left
-
-  -- f' is real C¹
-  have f'_is_real_C1 : ContDiff ℝ 1 (fderiv ℝ f) :=
-    (contDiff_succ_iff_fderiv.1 f_is_real_C2).right
-
-  -- f' is real differentiable
-  have f'_is_differentiable : Differentiable ℝ (fderiv ℝ f) :=
-    (contDiff_succ_iff_fderiv.1 f'_is_real_C1).left
-
-  -- Partial derivative in direction 1
-  let f_1 := fun w ↦ (fderiv ℝ f w) 1
-
-  -- Partial derivative in direction I
-  let f_I := fun w ↦ (fderiv ℝ f w) Complex.I
+    exact (partialDeriv_contDiff f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
 
   constructor
   · -- f is two times real continuously differentiable
     exact f_is_real_C2
 
   · -- Laplace of f is zero
-    intro z
     unfold Complex.laplace
-
     rw [CauchyRiemann₄ h]
     rw [partialDeriv_smul fI_is_real_differentiable]
-
-
-    have t₂ : (fderiv ℝ f_1 z) Complex.I = (fderiv ℝ f_I z) 1 := by
-      let B := l₂ f_is_real_C2 z Complex.I 1
-      rw [← B]
-      let A := derivSymm f f_is_real_C2 z 1 Complex.I
-      rw [A]
-      let C := l₂ f_is_real_C2 z 1 Complex.I
-      rw [C]
-    simp
-    rw [t₂]
-
-    conv =>
-      left
-      right
-      arg 2
-      arg 1
-      arg 2
-      intro z
-      simp [f_I]
-      rw [CauchyRiemann₁ (h z)]
-
-    rw [t₁a]
-
-    simp
-    rw [← mul_assoc]
+    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
+    rw [CauchyRiemann₄ h]
+    rw [partialDeriv_smul fI_is_real_differentiable]
+    rw [← smul_assoc]
     simp
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 9b2718f..20c68d6 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -42,3 +42,52 @@ theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n +
   refine ContDiff.clm_apply ?hg.h.hf ?hg.h.hg
   exact contDiff_id
   exact contDiff_const
+
+
+lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
+    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
+  rw [fderiv_clm_apply]
+  · simp
+  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
+  · simp
+
+
+lemma derivSymm (f : ℂ → ℂ) (hf : ContDiff ℝ 2 f) :
+  ∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
+  intro z a b
+
+  let f' := fderiv ℝ f
+  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
+    have h : Differentiable ℝ f := by
+      exact (contDiff_succ_iff_fderiv.1 hf).left
+    exact fun y => DifferentiableAt.hasFDerivAt (h y)
+
+  let f'' := (fderiv ℝ f' z)
+  have h₁ : HasFDerivAt f' f'' z := by
+    apply DifferentiableAt.hasFDerivAt
+    let A := (contDiff_succ_iff_fderiv.1 hf).right
+    let B := (contDiff_succ_iff_fderiv.1 A).left
+    simp at B
+    exact B z
+
+  let A := second_derivative_symmetric h₀ h₁ a b
+  dsimp [f'', f'] at A
+  apply A
+
+
+theorem partialDeriv_comm {f : ℂ → ℂ} (h : ContDiff ℝ 2 f) :
+  ∀ v₁ v₂ : ℂ, Real.partialDeriv v₁ (Real.partialDeriv v₂ f) = Real.partialDeriv v₂ (Real.partialDeriv v₁ f) := by
+
+  intro v₁ v₂
+  unfold Real.partialDeriv
+  funext z
+
+  conv =>
+    left
+    rw [← l₂ h z v₂ v₁]
+
+  rw [derivSymm f h z v₁ v₂]
+
+  conv =>
+    left
+    rw [l₂ h z v₁ v₂]