split off file

Nevanlinna/complexHarmonic.examples.lean

@@ -0,0 +1,325 @@
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+import Mathlib.Data.Complex.Module
+import Mathlib.Data.Complex.Order
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Topology.Algebra.InfiniteSum.Module
+import Mathlib.Topology.Instances.RealVectorSpace
+import Nevanlinna.cauchyRiemann
+import Nevanlinna.laplace
+import Nevanlinna.complexHarmonic
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
+variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁]
+
+
+theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
+  Harmonic f := by
+
+  -- f is real C²
+  have f_is_real_C2 : ContDiff ℝ 2 f :=
+    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+
+  have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by
+    exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
+
+  constructor
+  · -- f is two times real continuously differentiable
+    exact f_is_real_C2
+
+  · -- Laplace of f is zero
+    unfold Complex.laplace
+    rw [CauchyRiemann₄ h]
+
+    -- This lemma says that partial derivatives commute with complex scalar
+    -- multiplication. This is a consequence of partialDeriv_compContLin once we
+    -- note that complex scalar multiplication is continuous ℝ-linear.
+    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
+      intro v s g hg
+
+      -- Present scalar multiplication as a continuous ℝ-linear map. This is
+      -- horrible, there must be better ways to do that.
+      let sMuls : F₁ →L[ℝ] F₁ :=
+      {
+        toFun := fun x ↦ s • x
+        map_add' := by exact fun x y => DistribSMul.smul_add s x y
+        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
+        cont := continuous_const_smul s
+      }
+
+      -- Bring the goal into a form that is recognized by
+      -- partialDeriv_compContLin.
+      have : s • g = sMuls ∘ g := by rfl
+      rw [this]
+
+      rw [partialDeriv_compContLin ℝ hg]
+      rfl
+
+    rw [this]
+    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
+    rw [CauchyRiemann₄ h]
+    rw [this]
+    rw [← smul_assoc]
+    simp
+
+    -- Subgoals coming from the application of 'this'
+    -- Differentiable ℝ (Real.partialDeriv 1 f)
+    exact fI_is_real_differentiable
+    -- Differentiable ℝ (Real.partialDeriv 1 f)
+    exact fI_is_real_differentiable
+
+
+theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpen s) (h : DifferentiableOn ℂ f s) :
+  HarmonicOn f s := by
+
+  -- f is real C²
+  have f_is_real_C2 : ContDiffOn ℝ 2 f s :=
+    ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h hs)
+
+  constructor
+  · -- f is two times real continuously differentiable
+    exact f_is_real_C2
+
+  · -- Laplace of f is zero
+    unfold Complex.laplace
+    intro z hz
+    simp
+    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+      unfold Filter.EventuallyEq
+      unfold Filter.Eventually
+      simp
+      refine mem_nhds_iff.mpr ?_
+      use s
+      constructor
+      · intro x hx
+        simp
+        apply CauchyRiemann₅
+        apply DifferentiableOn.differentiableAt h
+        exact IsOpen.mem_nhds hs hx
+      · constructor
+        · exact hs
+        · exact hz
+    rw [partialDeriv_eventuallyEq ℝ this Complex.I]
+    rw [partialDeriv_smul'₂]
+
+    simp
+    rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz]
+
+    have : Complex.I • partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z = Complex.I • (partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z) := by
+      rfl
+    rw [this]
+    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
+      unfold Filter.EventuallyEq
+      unfold Filter.Eventually
+      simp
+      refine mem_nhds_iff.mpr ?_
+      use s
+      constructor
+      · intro x hx
+        simp
+        apply CauchyRiemann₅
+        apply DifferentiableOn.differentiableAt h
+        exact IsOpen.mem_nhds hs hx
+      · constructor
+        · exact hs
+        · exact hz
+    rw [partialDeriv_eventuallyEq ℝ this 1]
+    rw [partialDeriv_smul'₂]
+    simp
+    rw [← smul_assoc]
+    simp
+
+
+theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
+  Harmonic (Complex.reCLM ∘ f) := by
+  apply harmonic_comp_CLM_is_harmonic
+  exact holomorphic_is_harmonic h
+
+
+theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
+  Harmonic (Complex.imCLM ∘ f) := by
+  apply harmonic_comp_CLM_is_harmonic
+  exact holomorphic_is_harmonic h
+
+
+theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
+  Harmonic (Complex.conjCLE ∘ f) := by
+  apply harmonic_iff_comp_CLE_is_harmonic.1
+  exact holomorphic_is_harmonic h
+
+
+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
+    (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
+
+  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
+      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
+      rw [Complex.normSq_eq_conj_mul_self]
+    rw [this]
+    exact hyp
+
+
+  -- 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
+    intro z hz
+    unfold Function.comp
+    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)
+      simp
+      tauto
+    rw [this]
+    simp
+    constructor
+    · exact Real.pi_pos
+    · exact Real.pi_nonneg
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
+    exact h₂ z hz
+
+  rw [HarmonicOn_congr hs this]
+  simp
+
+  apply harmonicOn_add_harmonicOn_is_harmonicOn hs
+
+  have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by
+    rfl
+  rw [this]
+
+  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
+  have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by
+    intro z hz
+    unfold Function.comp
+    rw [Complex.log_conj]
+    rfl
+    exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
+  rw [HarmonicOn_congr hs this]
+
+  rw [← harmonicOn_iff_comp_CLE_is_harmonicOn]
+
+  apply holomorphicOn_is_harmonicOn
+  exact hs
+
+  intro z hz
+  apply DifferentiableAt.differentiableWithinAt
+  apply DifferentiableAt.comp
+
+
+
+  exact Complex.differentiableAt_log (h₃ z hz)
+  apply DifferentiableOn.differentiableAt h₁ -- (h₁ z hz)
+  exact IsOpen.mem_nhds hs hz
+  exact hs
+
+  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
+  apply holomorphicOn_is_harmonicOn hs
+  exact DifferentiableOn.clog h₁ h₃
+
+
+theorem log_normSq_of_holomorphic_is_harmonic
+  {f : ℂ → ℂ}
+  (h₁ : Differentiable ℂ f)
+  (h₂ : ∀ z, f z ≠ 0)
+  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
+  Harmonic (Real.log ∘ Complex.normSq ∘ f) := 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 : 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
+      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
+      rw [Complex.normSq_eq_conj_mul_self]
+    rw [this]
+    exact hyp
+
+
+  -- 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
+    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)
+      simp
+      tauto
+    rw [this]
+    simp
+    constructor
+    · exact Real.pi_pos
+    · exact Real.pi_nonneg
+    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
+    exact h₂ z
+  rw [this]
+
+  apply harmonic_add_harmonic_is_harmonic
+  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
+    funext z
+    unfold Function.comp
+    rw [Complex.log_conj]
+    rfl
+    exact Complex.slitPlane_arg_ne_pi (h₃ z)
+  rw [this]
+  rw [← harmonic_iff_comp_CLE_is_harmonic]
+
+  repeat
+    apply holomorphic_is_harmonic
+    intro z
+    apply DifferentiableAt.comp
+    exact Complex.differentiableAt_log (h₃ z)
+    exact h₁ z
+
+
+theorem logabs_of_holomorphic_is_harmonic
+  {f : ℂ → ℂ}
+  (h₁ : Differentiable ℂ f)
+  (h₂ : ∀ z, f z ≠ 0)
+  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
+  Harmonic (fun z ↦ Real.log ‖f z‖) := by
+
+  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
+  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
+    funext z
+    simp
+    unfold Complex.abs
+    simp
+    rw [Real.log_sqrt]
+    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
+    exact Complex.normSq_nonneg (f z)
+  rw [this]
+
+  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
+  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
+
+  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃

Nevanlinna/complexHarmonic.lean

@@ -189,306 +189,3 @@ theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {
       simp
     nth_rewrite 2 [this]
     exact harmonicOn_comp_CLM_is_harmonicOn hs
-
-
-theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
-  Harmonic f := by
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiff ℝ 2 f :=
-    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
-
-  have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by
-    exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
-
-  constructor
-  · -- f is two times real continuously differentiable
-    exact f_is_real_C2
-
-  · -- Laplace of f is zero
-    unfold Complex.laplace
-    rw [CauchyRiemann₄ h]
-
-    -- This lemma says that partial derivatives commute with complex scalar
-    -- multiplication. This is a consequence of partialDeriv_compContLin once we
-    -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
-      intro v s g hg
-
-      -- Present scalar multiplication as a continuous ℝ-linear map. This is
-      -- horrible, there must be better ways to do that.
-      let sMuls : F₁ →L[ℝ] F₁ :=
-      {
-        toFun := fun x ↦ s • x
-        map_add' := by exact fun x y => DistribSMul.smul_add s x y
-        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
-        cont := continuous_const_smul s
-      }
-
-      -- Bring the goal into a form that is recognized by
-      -- partialDeriv_compContLin.
-      have : s • g = sMuls ∘ g := by rfl
-      rw [this]
-
-      rw [partialDeriv_compContLin ℝ hg]
-      rfl
-
-    rw [this]
-    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
-    rw [CauchyRiemann₄ h]
-    rw [this]
-    rw [← smul_assoc]
-    simp
-
-    -- Subgoals coming from the application of 'this'
-    -- Differentiable ℝ (Real.partialDeriv 1 f)
-    exact fI_is_real_differentiable
-    -- Differentiable ℝ (Real.partialDeriv 1 f)
-    exact fI_is_real_differentiable
-
-
-theorem holomorphicOn_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} (hs : IsOpen s) (h : DifferentiableOn ℂ f s) :
-  HarmonicOn f s := by
-
-  -- f is real C²
-  have f_is_real_C2 : ContDiffOn ℝ 2 f s :=
-    ContDiffOn.restrict_scalars ℝ (DifferentiableOn.contDiffOn h hs)
-
-  constructor
-  · -- f is two times real continuously differentiable
-    exact f_is_real_C2
-
-  · -- Laplace of f is zero
-    unfold Complex.laplace
-    intro z hz
-    simp
-    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
-      unfold Filter.EventuallyEq
-      unfold Filter.Eventually
-      simp
-      refine mem_nhds_iff.mpr ?_
-      use s
-      constructor
-      · intro x hx
-        simp
-        apply CauchyRiemann₅
-        apply DifferentiableOn.differentiableAt h
-        exact IsOpen.mem_nhds hs hx
-      · constructor
-        · exact hs
-        · exact hz
-    rw [partialDeriv_eventuallyEq ℝ this Complex.I]
-    rw [partialDeriv_smul'₂]
-
-    simp
-    rw [partialDeriv_commOn hs f_is_real_C2 Complex.I 1 z hz]
-
-    have : Complex.I • partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z = Complex.I • (partialDeriv ℝ 1 (partialDeriv ℝ Complex.I f) z) := by
-      rfl
-    rw [this]
-    have : partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by
-      unfold Filter.EventuallyEq
-      unfold Filter.Eventually
-      simp
-      refine mem_nhds_iff.mpr ?_
-      use s
-      constructor
-      · intro x hx
-        simp
-        apply CauchyRiemann₅
-        apply DifferentiableOn.differentiableAt h
-        exact IsOpen.mem_nhds hs hx
-      · constructor
-        · exact hs
-        · exact hz
-    rw [partialDeriv_eventuallyEq ℝ this 1]
-    rw [partialDeriv_smul'₂]
-    simp
-    rw [← smul_assoc]
-    simp
-
-
-theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.reCLM ∘ f) := by
-  apply harmonic_comp_CLM_is_harmonic
-  exact holomorphic_is_harmonic h
-
-
-theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.imCLM ∘ f) := by
-  apply harmonic_comp_CLM_is_harmonic
-  exact holomorphic_is_harmonic h
-
-
-theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
-  Harmonic (Complex.conjCLE ∘ f) := by
-  apply harmonic_iff_comp_CLE_is_harmonic.1
-  exact holomorphic_is_harmonic h
-
-
-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
-    (harmonicOn_comp_CLM_is_harmonicOn hs hyp : HarmonicOn (Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f) s)
-
-  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
-      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
-      rw [Complex.normSq_eq_conj_mul_self]
-    rw [this]
-    exact hyp
-
-
-  -- 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
-    intro z hz
-    unfold Function.comp
-    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)
-      simp
-      tauto
-    rw [this]
-    simp
-    constructor
-    · exact Real.pi_pos
-    · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz)
-    exact h₂ z hz
-
-  rw [HarmonicOn_congr hs this]
-  simp
-
-  apply harmonicOn_add_harmonicOn_is_harmonicOn hs
-
-  have : (fun x => Complex.log ((starRingEnd ℂ) (f x))) = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) := by
-    rfl
-  rw [this]
-
-  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
-  have : ∀ z ∈ s, (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) z = (Complex.conjCLE ∘ Complex.log ∘ f) z := by
-    intro z hz
-    unfold Function.comp
-    rw [Complex.log_conj]
-    rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z hz)
-  rw [HarmonicOn_congr hs this]
-
-  rw [← harmonicOn_iff_comp_CLE_is_harmonicOn]
-
-  apply holomorphicOn_is_harmonicOn
-  exact hs
-
-  intro z hz
-  apply DifferentiableAt.differentiableWithinAt
-  apply DifferentiableAt.comp
-
-
-
-  exact Complex.differentiableAt_log (h₃ z hz)
-  apply DifferentiableOn.differentiableAt h₁ -- (h₁ z hz)
-  exact IsOpen.mem_nhds hs hz
-  exact hs
-
-  -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
-  apply holomorphicOn_is_harmonicOn hs
-  exact DifferentiableOn.clog h₁ h₃
-
-
-theorem log_normSq_of_holomorphic_is_harmonic
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (Real.log ∘ Complex.normSq ∘ f) := 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 : 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
-      rw [Complex.ofReal_log (Complex.normSq_nonneg (f z))]
-      rw [Complex.normSq_eq_conj_mul_self]
-    rw [this]
-    exact hyp
-
-
-  -- 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
-    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)
-      simp
-      tauto
-    rw [this]
-    simp
-    constructor
-    · exact Real.pi_pos
-    · exact Real.pi_nonneg
-    exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
-    exact h₂ z
-  rw [this]
-
-  apply harmonic_add_harmonic_is_harmonic
-  have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
-    funext z
-    unfold Function.comp
-    rw [Complex.log_conj]
-    rfl
-    exact Complex.slitPlane_arg_ne_pi (h₃ z)
-  rw [this]
-  rw [← harmonic_iff_comp_CLE_is_harmonic]
-
-  repeat
-    apply holomorphic_is_harmonic
-    intro z
-    apply DifferentiableAt.comp
-    exact Complex.differentiableAt_log (h₃ z)
-    exact h₁ z
-
-
-theorem logabs_of_holomorphic_is_harmonic
-  {f : ℂ → ℂ}
-  (h₁ : Differentiable ℂ f)
-  (h₂ : ∀ z, f z ≠ 0)
-  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
-  Harmonic (fun z ↦ Real.log ‖f z‖) := by
-
-  -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f)
-  have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
-    funext z
-    simp
-    unfold Complex.abs
-    simp
-    rw [Real.log_sqrt]
-    rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
-    exact Complex.normSq_nonneg (f z)
-  rw [this]
-
-  -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f)
-  apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1
-
-  exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃