From 80486cc56cf7d85b2f8bb7387db0f20eb644f510 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 4 Jun 2024 12:30:25 +0200
Subject: [PATCH] working

---
 Nevanlinna/laplace.lean      | 71 ++++++++++++++++++++++++++++++++++++
 Nevanlinna/partialDeriv.lean | 15 ++++++++
 2 files changed, 86 insertions(+)

diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index 2bc04a9..313a1d3 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -131,6 +131,77 @@ theorem laplace_add_ContDiffOn
   rw [add_comm]
 
 
+theorem laplace_add_ContDiffAt
+  {f₁ f₂ : ℂ → F}
+  {x : ℂ}
+  (h₁ : ContDiffAt ℝ 2 f₁ x)
+  (h₂ : ContDiffAt ℝ 2 f₂ x) :
+  Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
+
+  unfold Complex.laplace
+  simp
+
+  have hf₁ : ∀ z ∈ s, DifferentiableAt ℝ f₁ z := by
+    intro z hz
+    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+    apply ContDiffOn.differentiableOn h₁ one_le_two
+
+  have hf₂ : ∀ z ∈ s, DifferentiableAt ℝ f₂ z := by
+    intro z hz
+    convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+    apply ContDiffOn.differentiableOn h₂ one_le_two
+
+  have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use s
+    constructor
+    · exact IsOpen.mem_nhds hs hx
+    · intro z hz
+      apply partialDeriv_add₂_differentiableAt
+      exact hf₁ z hz
+      exact hf₂ z hz
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
+    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
+    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
+
+  have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use s
+    constructor
+    · exact IsOpen.mem_nhds hs hx
+    · intro z hz
+      apply partialDeriv_add₂_differentiableAt
+      exact hf₁ z hz
+      exact hf₂ z hz
+  rw [partialDeriv_eventuallyEq ℝ this]
+  have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
+    let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
+    let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
+    let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
+  rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
+
+  -- I am super confused at this point because the tactic 'ring' does not work.
+  -- I do not understand why. So, I need to do things by hand.
+  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} : ∀ v : ℝ, Δ (v • f) = v • (Δ f) := by
   intro v
   unfold Complex.laplace
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index b2a1b8a..1285eb2 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -85,6 +85,21 @@ theorem partialDeriv_add₂_differentiableAt
   rfl
 
 
+theorem partialDeriv_add₂_differentiableAt'
+  {f₁ f₂ : E → F}
+  {v : E}
+  {x : E}
+  (h₁ : DifferentiableAt 𝕜 f₁ x)
+  (h₂ : DifferentiableAt 𝕜 f₂ x) :
+  partialDeriv 𝕜 v (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := 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