Update complexHarmonic.lean

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} (h : HarmonicOn f s) :
+theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (hs : IsOpen s) (h : HarmonicOn f s) :
   HarmonicOn (l ∘ f) s := by
 
   constructor
@@ -97,15 +97,14 @@ theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l :
     apply ContDiffOn.continuousLinearMap_comp
     exact h.1
   · -- Vanishing of Laplace
-
-    rw [laplace_compContLin]
-    simp
     intro z zHyp
+    rw [laplace_compContLinAt]
+    simp
     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₁} :
@@ -200,15 +199,16 @@ 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 : Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) from
-    (harmonic_comp_CLM_is_harmonic hyp : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f))
+  suffices hyp : HarmonicOn (⇑Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s from
+    (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
 
-  suffices hyp : Harmonic (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) from by
+  suffices hyp : HarmonicOn (Complex.log ∘ (((starRingEnd ℂ) ∘ f) * f)) s 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 : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
+  have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := 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)
+        exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
       simp
       tauto
     rw [this]
@@ -237,8 +237,9 @@ 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)
-    exact h₂ z
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
+    exact h₂ z hz
+  
   rw [this]
 
   apply harmonic_add_harmonic_is_harmonic