From a2c2d05789ceaae0022605bf4addd08e97180904 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 10:52:12 +0200
Subject: [PATCH] Working

---
 Nevanlinna/holomorphic.examples.lean | 108 +++++++++++++++++----------
 Nevanlinna/partialDeriv.lean         |  14 ++++
 2 files changed, 83 insertions(+), 39 deletions(-)

diff --git a/Nevanlinna/holomorphic.examples.lean b/Nevanlinna/holomorphic.examples.lean
index 9dd4bbf..26972ee 100644
--- a/Nevanlinna/holomorphic.examples.lean
+++ b/Nevanlinna/holomorphic.examples.lean
@@ -114,56 +114,86 @@ theorem harmonic_is_realOfHolomorphic
 
   let g : ℂ → ℂ := f_1 - Complex.I • f_I
 
-  have reg₀ : Differentiable ℝ g := by 
-    let smulICLM : ℂ ≃L[ℝ] ℂ :=
-    {
-      toFun := fun x ↦ Complex.I • x
-      map_add' := fun x y => DistribSMul.smul_add Complex.I x y
-      map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) Complex.I x).symm
-      invFun := fun x ↦ (Complex.I)⁻¹ • x
-      left_inv := by
-        intro x
-        simp
-        rw [← mul_assoc, mul_comm]
-        simp
-      right_inv := by
-        intro x
-        simp
-        rw [← mul_assoc]
-        simp
-      continuous_toFun := continuous_const_smul Complex.I
-      continuous_invFun := continuous_const_smul (Complex.I)⁻¹
-    }
-
-    apply Differentiable.sub
-    apply Differentiable.comp
-    exact ContinuousLinearMap.differentiable Complex.ofRealCLM
+  have reg₂f : ContDiff ℝ 2 f := by
+    apply contDiff_iff_contDiffAt.mpr 
     intro z
-    sorry
-    apply Differentiable.comp
-    sorry
-    sorry
+    exact (hf z).1
 
+  have reg₁f_1 : ContDiff ℝ 1 f_1 := by
+    apply contDiff_iff_contDiffAt.mpr 
+    intro z
+    dsimp [f_1]
+    apply ContDiffAt.continuousLinearMap_comp
+    exact partialDeriv_contDiffAt ℝ (hf z).1 1
+
+  have reg₁f_I : ContDiff ℝ 1 f_I := by
+    apply contDiff_iff_contDiffAt.mpr 
+    intro z
+    dsimp [f_I]
+    apply ContDiffAt.continuousLinearMap_comp
+    exact partialDeriv_contDiffAt ℝ (hf z).1 Complex.I
+
+  have reg₁g : ContDiff ℝ 1 g := by 
+    dsimp [g]
+    apply ContDiff.sub
+    exact reg₁f_1
+    have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+    rw [this]
+    apply ContDiff.const_smul
+    exact reg₁f_I
   
   have reg₁ : Differentiable ℂ g := by 
     intro z
     apply CauchyRiemann₇.2
     constructor
-    · exact reg₀ z
+    · apply Differentiable.differentiableAt
+      apply ContDiff.differentiable
+      exact reg₁g
+      rfl
     · dsimp [g]
-      have : f_1 - Complex.I • f_I = f_1 + (- Complex.I • f_I) := by
-        rw [sub_eq_add_neg]
-        simp
-      rw [this, partialDeriv_add₂, partialDeriv_add₂]
+      rw [partialDeriv_sub₂, partialDeriv_sub₂]
       simp
       dsimp [f_1, f_I]
-      
-      sorry
-      sorry
-      sorry
-      sorry
-      sorry
+      rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
+      rw [partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin]
+      rw [mul_sub]
+      simp
+      rw [← mul_assoc]
+      simp
+      rw [add_comm, sub_eq_add_neg]
+      congr 1
+      · rw [partialDeriv_comm reg₂f Complex.I 1]
+      · let A := Filter.EventuallyEq.eq_of_nhds (hf z).2
+        simp at A
+        unfold Complex.laplace at A
+        conv =>
+          right
+          right
+          rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) z)]
+          rw [← A]
+        simp
 
+      --Differentiable ℝ (partialDeriv ℝ _ f)
+      repeat
+        apply ContDiff.differentiable 
+        apply contDiff_iff_contDiffAt.mpr 
+        exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).1 _
+        apply le_rfl
+      -- Differentiable ℝ f_1
+      exact reg₁f_1.differentiable le_rfl
+      -- Differentiable ℝ (Complex.I • f_I)
+      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+      rw [this]
+      apply Differentiable.const_smul
+      exact reg₁f_I.differentiable le_rfl
+      -- Differentiable ℝ f_1
+      exact reg₁f_1.differentiable le_rfl
+      -- Differentiable ℝ (Complex.I • f_I)
+      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
+      rw [this]
+      apply Differentiable.const_smul
+      exact reg₁f_I.differentiable le_rfl
+  
   
 
 
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 520b6a4..a2d819e 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -102,6 +102,20 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
   simp
 
 
+theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
+  unfold partialDeriv
+  intro v
+  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
+  rw [this]
+  conv =>
+    left
+    intro w
+    left
+    rw [fderiv_sub (h₁ w) (h₂ w)]
+  funext w
+  simp
+
+
 theorem partialDeriv_add₂_differentiableAt
   {f₁ f₂ : E → F}
   {v : E}