From 7319bf60c0242e20548098cd2af921922e19acc5 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 18 May 2024 12:13:30 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 94 +++++++++++++++++++++++++++++++++
 1 file changed, 94 insertions(+)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 6537af8..fb0aefa 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -26,6 +26,23 @@ def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
+def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop :=
+  (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Complex.laplace f z = 0)
+
+
+theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) :
+  HarmonicOn f s := by
+  constructor
+  · apply contDiffOn_of_locally_contDiffOn
+    intro x xHyp
+    obtain ⟨u, uHyp⟩  := h x xHyp
+    use u
+    exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩ 
+  · intro x xHyp
+    obtain ⟨u, uHyp⟩  := h x xHyp
+    exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩
+
+
 theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) :
   Harmonic (f₁ + f₂) := by
   constructor
@@ -72,6 +89,21 @@ 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) :
+  HarmonicOn (l ∘ f) s := by
+
+  constructor
+  · -- Continuous differentiability
+    apply ContDiffOn.continuousLinearMap_comp
+    exact h.1
+  · rw [laplace_compContLin]
+    simp
+    intro z zHyp
+    rw [h.2 z]
+    simp
+    assumption
+
+
 theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
   Harmonic f ↔ Harmonic (l ∘ f) := by
 
@@ -161,6 +193,68 @@ theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f)
   exact holomorphic_is_harmonic h
 
 
+theorem log_normSq_of_holomorphicOn_is_harmonicOn
+  {f : ℂ → ℂ}
+  {s : Set ℂ}
+  (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 : 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 log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)