working

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

Nevanlinna/laplace.lean

@@ -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