Nevanlinna/complexHarmonic.lean

@@ -89,7 +89,7 @@ theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}
     exact ContDiff.restrict_scalars ℝ h.1
 
 
-theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (hs : IsOpen s) (h : HarmonicOn f s) :
+theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (h : HarmonicOn f s) :
   HarmonicOn (l ∘ f) s := by
 
   constructor
@@ -97,14 +97,15 @@ theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l :
     apply ContDiffOn.continuousLinearMap_comp
     exact h.1
   · -- Vanishing of Laplace
-    intro z zHyp
+
-    rw [laplace_compContLinAt]
+    rw [laplace_compContLin]
     simp
+    intro z zHyp
     rw [h.2 z]
     simp
     assumption
-    apply ContDiffOn.contDiffAt h.1
+
-    exact IsOpen.mem_nhds hs zHyp
+
 
 
 theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@@ -199,16 +200,15 @@ theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f)
 theorem log_normSq_of_holomorphicOn_is_harmonicOn
   {f : ℂ → ℂ}
   {s : Set ℂ}
-  (hs : IsOpen s)
   (h₁ : DifferentiableOn ℂ f s)
   (h₂ : ∀ z ∈ s, f z ≠ 0)
   (h₃ : ∀ z ∈ s, f z ∈ Complex.slitPlane) :
   HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by
 
-  suffices hyp : HarmonicOn (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s from
+  suffices hyp : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
+    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
 
-  suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) s from by
+  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
     have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f) := by
       funext z
       simp
@@ -220,16 +220,16 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
 
   -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f)
   -- THIS IS WHERE WE USE h₃
-  have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := by
+  have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
-    intro z hz
     unfold Function.comp
+    funext z
     simp
     rw [Complex.log_mul_eq_add_log_iff]
 
     have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
       rw [Complex.arg_conj]
       have : ¬ Complex.arg (f z) = Real.pi := by
-        exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
+        exact Complex.slitPlane_arg_ne_pi (h₃ z)
       simp
       tauto
     rw [this]
@@ -237,9 +237,8 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
     constructor
     · exact Real.pi_pos
     · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
-    exact h₂ z hz
+    exact h₂ z
-  
   rw [this]
 
   apply harmonic_add_harmonic_is_harmonic