From 7f10e2852523c5b1b3d04afd15b51a1fa10c256b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 30 May 2024 10:41:10 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index f573576..577b52d 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/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