Nevanlinna/complexHarmonic.lean

@@ -43,50 +43,6 @@ theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀
     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
@@ -98,17 +54,6 @@ 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
@@ -295,8 +240,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
     exact h₂ z hz
   
-  rw [HarmonicOn_congr hs this]
-  simp
+  rw [this]
 
   apply harmonic_add_harmonic_is_harmonic
   have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by

Nevanlinna/laplace.lean

@@ -24,13 +24,6 @@ noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
   fun f ↦ partialDeriv ℝ 1 (partialDeriv ℝ 1 f) + partialDeriv ℝ Complex.I (partialDeriv ℝ Complex.I f)
 
 
-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₂]
@@ -53,37 +46,6 @@ 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

@@ -128,15 +128,6 @@ 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 𝕜]