From c2c730e510071f911b3d890edd0358c8f27e9b76 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 3 Jun 2024 13:35:53 +0200
Subject: [PATCH] All done.

---
 Nevanlinna/complexHarmonic.lean |  6 +----
 Nevanlinna/laplace.lean         | 42 ++++++++++++++++++++++++++++-----
 2 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 8ce9bcd..398e6ef 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -407,11 +407,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
 
   -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
   apply holomorphicOn_is_harmonicOn hs
-  apply?
-
-
-  exact h₁ z
-
+  exact DifferentiableOn.clog h₁ h₃
 
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index 5a9b1ac..2025d0c 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -65,22 +65,52 @@ theorem laplace_add_ContDiffOn
   simp
   intro x hx
 
+  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
-    sorry
+    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
-    sorry
+    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
-    sorry
+    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
-    sorry
+    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
-    sorry
+    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
-    sorry
+    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.