working

Nevanlinna/complexHarmonic.lean

@@ -35,14 +35,58 @@ theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀
   constructor
   · apply contDiffOn_of_locally_contDiffOn
     intro x xHyp
-    obtain ⟨u, uHyp⟩  := h x xHyp
+    obtain ⟨u, uHyp⟩ := h x xHyp
     use u
     exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩
   · intro x xHyp
-    obtain ⟨u, uHyp⟩  := h x xHyp
+    obtain ⟨u, uHyp⟩ := h x xHyp
     exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
 
 
+theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) :
+  HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by
+  constructor
+  · intro h₁
+    constructor
+    · apply ContDiffOn.congr h₁.1
+      intro x hx
+      rw [eq_comm]
+      exact hf₁₂ x hx
+    · intro z hz
+      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
+  · intro h₁
+    constructor
+    · apply ContDiffOn.congr h₁.1
+      intro x hx
+      exact hf₁₂ x hx
+    · intro z hz
+      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
+
+
 theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
   Harmonic (f₁ + f₂) := by
   constructor
@@ -54,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
@@ -240,7 +295,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
     exact h₂ z hz
   
-  rw [this]
+  rw [HarmonicOn_congr hs this]
+  simp
 
   apply harmonic_add_harmonic_is_harmonic
   have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by

Nevanlinna/laplace.lean

@@ -24,7 +24,14 @@ noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
   fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
 
 
-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_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Complex.laplace f₁ x = Complex.laplace f₂ x := by
+  unfold Complex.laplace
+  simp
+  rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h 1) 1]
+  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
   unfold Complex.laplace
   rw [partialDeriv_add₂]
   rw [partialDeriv_add₂]
@@ -46,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

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
@@ -128,6 +128,15 @@ theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[n
   exact fun v => rfl
 
 
+theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ =ᶠ[nhds x] partialDeriv 𝕜 v f₂ := by
+  unfold partialDeriv
+  intro v
+  let A : fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f₂ := Filter.EventuallyEq.fderiv h
+  apply Filter.EventuallyEq.comp₂ 
+  exact A
+  simp
+
+
 section restrictScalars
 
 variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]