From a7b0790675adb3f5a1e69cd5eaf3116200b6a357 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 31 May 2024 09:21:35 +0200
Subject: [PATCH] working

---
 Nevanlinna/laplace.lean      | 54 +++++++++++++++++++++---------------
 Nevanlinna/partialDeriv.lean | 20 +++++++++++--
 2 files changed, 50 insertions(+), 24 deletions(-)

diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index 46fdad8..811806d 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -53,35 +53,45 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ :
   exact h₂.differentiable one_le_two
 
 
-theorem laplace_add_ContDiffOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (h₁ : ContDiffOn ℝ 2 f₁ s) (h₂ : ContDiffOn ℝ 2 f₂ s): ∀ x ∈ s, Complex.laplace (f₁ + f₂) x = (Complex.laplace f₁) x + (Complex.laplace f₂) x := by
+theorem laplace_add_ContDiffOn
+  {f₁ f₂ : ℂ → F}
+  {s : Set ℂ}
+  (hs : IsOpen s)
+  (h₁ : ContDiffOn ℝ 2 f₁ s)
+  (h₂ : ContDiffOn ℝ 2 f₂ s) :
+  ∀ x ∈ s, Complex.laplace (f₁ + f₂) x = (Complex.laplace f₁) x + (Complex.laplace f₂) x := by
 
   unfold Complex.laplace
   simp
   intro x hx
+
   have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
     sorry
   rw [partialDeriv_eventuallyEq ℝ this]
-  
+  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
+    sorry
+  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
+    sorry
+  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
 
-  rw [partialDeriv_add₂]
+  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
+    sorry
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
+    sorry
+  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
+    sorry
+  rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
 
-  rw [partialDeriv_add₂]
-  rw [partialDeriv_add₂]
-  rw [partialDeriv_add₂]
-  exact
-    add_add_add_comm (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁))
-      (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₂))
-      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁))
-      (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₂))
-
-  exact (partialDeriv_contDiff ℝ h₁ Complex.I).differentiable le_rfl
-  exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl
-  exact h₁.differentiable one_le_two
-  exact h₂.differentiable one_le_two
-  exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl
-  exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl
-  exact h₁.differentiable one_le_two
-  exact h₂.differentiable one_le_two
+  -- I am super confused at this point because the tactic 'ring' does not work.
+  -- I do not understand why.
+  rw [add_assoc]
+  rw [add_assoc]
+  rw [add_right_inj (partialDeriv ℝ 1 (partialDeriv ℝ 1 f₁) x)]
+  rw [add_comm]
+  rw [add_assoc]
+  rw [add_right_inj (partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f₁) x)]
+  rw [add_comm]
 
 
 theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
@@ -119,7 +129,7 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
 
   have A₂ : ∃ v ∈ nhds x, (IsOpen v) ∧ (x ∈ v) ∧ (ContDiffOn ℝ 2 f v) := by
     have : ∃ u ∈ nhds x, ContDiffOn ℝ 2 f u := by
-      apply ContDiffAt.contDiffOn h 
+      apply ContDiffAt.contDiffOn h
       rfl
     obtain ⟨u, hu₁, hu₂⟩ := this
     obtain ⟨v, hv₁, hv₂, hv₃⟩ := mem_nhds_iff.1 hu₁
@@ -130,7 +140,7 @@ theorem laplace_compContLinAt {f : ℂ → F} {l : F →L[ℝ] G} {x : ℂ} (h :
       exact hv₂
       constructor
       · exact hv₃
-      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁    
+      · exact ContDiffOn.congr_mono hu₂ (fun x => congrFun rfl) hv₁
   obtain ⟨v, hv₁, hv₂, hv₃, hv₄⟩ := A₂
 
   have D : ∀ w : ℂ, partialDeriv ℝ w (l ∘ f) =ᶠ[nhds x] l ∘ partialDeriv ℝ w (f) := by
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index e5fe2fe..4312e5e 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -54,6 +54,22 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
+theorem partialDeriv_add₂_differentiableAt
+  {f₁ f₂ : E → F}
+  {v : E}
+  {x : E}
+  (h₁ : DifferentiableAt 𝕜 f₁ x)
+  (h₂ : DifferentiableAt 𝕜 f₂ x)
+  :
+  partialDeriv 𝕜 v (f₁ + f₂) x = (partialDeriv 𝕜 v f₁) x + (partialDeriv 𝕜 v f₂) x := by
+
+  unfold partialDeriv
+  have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
+  rw [this]
+  rw [fderiv_add h₁ h₂]
+  rfl
+
+
 theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
   unfold partialDeriv
 
@@ -95,7 +111,7 @@ theorem partialDeriv_contDiffAt {n : ℕ} {f : E → F} {x : E} (h : ContDiffAt
   unfold partialDeriv
   intro v
 
-  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F := 
+  let eval_at_v : (E →L[𝕜] F) →L[𝕜] F :=
   {
     toFun := fun l ↦ l v
     map_add' := by simp
@@ -132,7 +148,7 @@ theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[
   unfold partialDeriv
   intro v
   let A : fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f₂ := Filter.EventuallyEq.fderiv h
-  apply Filter.EventuallyEq.comp₂ 
+  apply Filter.EventuallyEq.comp₂
   exact A
   simp