From c8e1aacb158fc21aa7add314bc112e7bb8a31b72 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 30 May 2024 17:02:15 +0200
Subject: [PATCH] working

---
 Nevanlinna/complexHarmonic.lean | 35 +++++++++++++++++++++++++++++----
 Nevanlinna/laplace.lean         | 33 ++++++++++++++++++++++++++++++-
 Nevanlinna/partialDeriv.lean    |  2 +-
 3 files changed, 64 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 81a70a5..12f91c5 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -57,8 +57,13 @@ theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (
         unfold Filter.EventuallyEq
         unfold Filter.Eventually
         simp
-        apply?
-        sorry
+        refine mem_nhds_iff.mpr ?_
+        use s
+        constructor 
+        · exact hf₁₂
+        · constructor
+          · exact hs
+          · exact hz
       rw [← laplace_eventuallyEq this]
       exact h₁.2 z hz
   · intro h₁
@@ -67,7 +72,17 @@ theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (
       intro x hx
       exact hf₁₂ x hx
     · intro z hz
-      have : f₁ =ᶠ[nhds z] f₂ := by sorry
+      have : f₁ =ᶠ[nhds z] f₂ := by 
+        unfold Filter.EventuallyEq
+        unfold Filter.Eventually
+        simp
+        refine mem_nhds_iff.mpr ?_
+        use s
+        constructor 
+        · exact hf₁₂
+        · constructor
+          · exact hs
+          · exact hz
       rw [laplace_eventuallyEq this]
       exact h₁.2 z hz
 
@@ -83,6 +98,17 @@ theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmon
     simp
 
 
+theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) :
+  HarmonicOn (f₁ + f₂) s := by
+  constructor
+  · exact ContDiffOn.add h₁.1 h₂.1
+  · rw [laplace_add h₁.1 h₂.1]
+    simp
+    intro z
+    rw [h₁.2 z, h₂.2 z]
+    simp
+
+
 theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) :
   Harmonic (c • f) := by
   constructor
@@ -268,7 +294,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     · exact Real.pi_nonneg
     exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
     exact h₂ z hz
-  rw [HarmonicOn_ext this]
+  
+  rw [HarmonicOn_congr hs this]
   simp
 
   apply harmonic_add_harmonic_is_harmonic
diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index b62f6e8..46fdad8 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -31,7 +31,7 @@ theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nh
   rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I]
 
 
-theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁)  (h₂ : ContDiff ℝ 2 f₂): Complex.laplace (f₁ + f₂) = (Complex.laplace f₁) + (Complex.laplace f₂) := by
+theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ : ContDiff ℝ 2 f₂): Complex.laplace (f₁ + f₂) = (Complex.laplace f₁) + (Complex.laplace f₂) := by
   unfold Complex.laplace
   rw [partialDeriv_add₂]
   rw [partialDeriv_add₂]
@@ -53,6 +53,37 @@ 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
+
+  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]
+  
+
+  rw [partialDeriv_add₂]
+
+  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
+
+
 theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
   intro v
   unfold Complex.laplace
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 9cddc27..e5fe2fe 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -42,7 +42,7 @@ theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiabl
     rw [fderiv_const_smul (h w)]
 
 
-theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁)  (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
+theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
   unfold partialDeriv
 
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl