import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv import Nevanlinna.complexHarmonic import Nevanlinna.holomorphic variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] theorem holomorphicAt_is_harmonicAt {f : ℂ → F₁} {z : ℂ} (hf : HolomorphicAt f z) : HarmonicAt f z := by let t := {x | HolomorphicAt f x} have ht : IsOpen t := HolomorphicAt_isOpen f have hz : z ∈ t := by exact hf constructor · -- ContDiffAt ℝ 2 f z exact HolomorphicAt_contDiffAt hf · -- Δ f =ᶠ[nhds z] 0 apply Filter.eventuallyEq_iff_exists_mem.2 use t constructor · exact IsOpen.mem_nhds ht hz · intro w hw unfold Complex.laplace simp rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ hw) Complex.I] rw [partialDeriv_smul'₂] simp rw [partialDeriv_commAt (HolomorphicAt_contDiffAt hw) Complex.I 1] rw [partialDeriv_eventuallyEq ℝ (CauchyRiemann'₆ hw) 1] rw [partialDeriv_smul'₂] simp rw [← smul_assoc] simp theorem re_of_holomorphicAt_is_harmonicAr {f : ℂ → ℂ} {z : ℂ} (h : HolomorphicAt f z) : HarmonicAt (Complex.reCLM ∘ f) z := by apply harmonicAt_comp_CLM_is_harmonicAt exact holomorphicAt_is_harmonicAt h theorem im_of_holomorphicAt_is_harmonicAt {f : ℂ → ℂ} {z : ℂ} (h : HolomorphicAt f z) : HarmonicAt (Complex.imCLM ∘ f) z := by apply harmonicAt_comp_CLM_is_harmonicAt exact holomorphicAt_is_harmonicAt h theorem antiholomorphicAt_is_harmonicAt {f : ℂ → ℂ} {z : ℂ} (h : HolomorphicAt f z) : HarmonicAt (Complex.conjCLE ∘ f) z := by apply harmonicAt_iff_comp_CLE_is_harmonicAt.1 exact holomorphicAt_is_harmonicAt h theorem log_normSq_of_holomorphicAt_is_harmonicAt {f : ℂ → ℂ} {z : ℂ} (h₁f : HolomorphicAt f z) (h₂f : f z ≠ 0) : HarmonicAt (Real.log ∘ Complex.normSq ∘ f) z := by -- For later use have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by rw [Complex.mem_slitPlane_iff, Complex.mem_slitPlane_iff] simp at hz rw [Complex.ext_iff] at hz push_neg at hz simp at hz simp by_contra contra push_neg at contra exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2 -- First prove the theorem for functions with image in the slitPlane have lem₁ : ∀ g : ℂ → ℂ, (HolomorphicAt g z) → (g z ≠ 0) → (g z ∈ Complex.slitPlane) → HarmonicAt (Real.log ∘ Complex.normSq ∘ g) z := by intro g h₁g h₂g h₃g -- Rewrite the log |g|² as Complex.log (g * gc) suffices hyp : HarmonicAt (Complex.log ∘ ((Complex.conjCLE ∘ g) * g)) z from by have : Real.log ∘ Complex.normSq ∘ g = Complex.reCLM ∘ Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g := by funext x simp rw [this] have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ g = Complex.log ∘ ((Complex.conjCLE ∘ g) * g) := by funext x simp rw [Complex.ofReal_log] rw [Complex.normSq_eq_conj_mul_self] exact Complex.normSq_nonneg (g x) rw [← this] at hyp apply harmonicAt_comp_CLM_is_harmonicAt hyp -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc -- This uses the assumption that g z is in Complex.slitPlane have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.log ∘ Complex.conjCLE ∘ g + Complex.log ∘ g) := by apply Filter.eventuallyEq_iff_exists_mem.2 use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ) constructor · apply ContinuousAt.preimage_mem_nhds · exact (HolomorphicAt_differentiableAt h₁g).continuousAt · apply IsOpen.mem_nhds apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne constructor · exact h₃g · exact h₂g · intro x hx simp rw [Complex.log_mul_eq_add_log_iff _ hx.2] rw [Complex.arg_conj] simp [Complex.slitPlane_arg_ne_pi hx.1] constructor · exact Real.pi_pos · exact Real.pi_nonneg simp apply hx.2 -- Locally around z, rewrite Complex.log (g * gc) as Complex.log g + Complex.log.gc -- This uses the assumption that g z is in Complex.slitPlane have : (Complex.log ∘ (Complex.conjCLE ∘ g * g)) =ᶠ[nhds z] (Complex.conjCLE ∘ Complex.log ∘ g + Complex.log ∘ g) := by apply Filter.eventuallyEq_iff_exists_mem.2 use g⁻¹' (Complex.slitPlane ∩ {0}ᶜ) constructor · apply ContinuousAt.preimage_mem_nhds · exact (HolomorphicAt_differentiableAt h₁g).continuousAt · apply IsOpen.mem_nhds apply IsOpen.inter Complex.isOpen_slitPlane isOpen_ne constructor · exact h₃g · exact h₂g · intro x hx simp rw [← Complex.log_conj] rw [Complex.log_mul_eq_add_log_iff _ hx.2] rw [Complex.arg_conj] simp [Complex.slitPlane_arg_ne_pi hx.1] constructor · exact Real.pi_pos · exact Real.pi_nonneg simp apply hx.2 apply Complex.slitPlane_arg_ne_pi hx.1 rw [HarmonicAt_eventuallyEq this] apply harmonicAt_add_harmonicAt_is_harmonicAt · rw [← harmonicAt_iff_comp_CLE_is_harmonicAt] apply holomorphicAt_is_harmonicAt apply HolomorphicAt_comp use Complex.slitPlane constructor · apply IsOpen.mem_nhds exact Complex.isOpen_slitPlane assumption · exact fun z a => Complex.differentiableAt_log a exact h₁g · apply holomorphicAt_is_harmonicAt apply HolomorphicAt_comp use Complex.slitPlane constructor · apply IsOpen.mem_nhds exact Complex.isOpen_slitPlane assumption · exact fun z a => Complex.differentiableAt_log a exact h₁g by_cases h₃f : f z ∈ Complex.slitPlane · exact lem₁ f h₁f h₂f h₃f · have : Complex.normSq ∘ f = Complex.normSq ∘ (-f) := by funext; simp rw [this] apply lem₁ (-f) · exact HolomorphicAt_neg h₁f · simpa · exact (slitPlaneLemma h₂f).resolve_left h₃f 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 : 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_holomorphicOn_is_harmonicOn {f : ℂ → ℂ} {s : Set ℂ} (hs : IsOpen s) (h₁ : DifferentiableOn ℂ f s) (h₂ : ∀ z ∈ s, f z ≠ 0) : HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s := by have slitPlaneLemma {z : ℂ} (hz : z ≠ 0) : z ∈ Complex.slitPlane ∨ -z ∈ Complex.slitPlane := by rw [Complex.mem_slitPlane_iff] rw [Complex.mem_slitPlane_iff] simp at hz rw [Complex.ext_iff] at hz push_neg at hz simp at hz simp by_contra contra push_neg at contra exact hz (le_antisymm contra.1.1 contra.2.1) contra.1.2 let s₁ : Set ℂ := { z | f z ∈ Complex.slitPlane} ∩ s have hs₁ : IsOpen s₁ := by let A := DifferentiableOn.continuousOn h₁ let B := continuousOn_iff'.1 A obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane have : u ∩ s = s₁ := by rw [← hu₂] tauto rw [← this] apply IsOpen.inter hu₁ hs have harm₁ : HarmonicOn (Real.log ∘ Complex.normSq ∘ f) s₁ := by apply log_normSq_of_holomorphicOn_is_harmonicOn' exact hs₁ apply DifferentiableOn.mono h₁ (Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s) -- ∀ z ∈ s₁, f z ≠ 0 exact fun z hz ↦ h₂ z (Set.mem_of_mem_inter_right hz) -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane intro z hz apply hz.1 let s₂ : Set ℂ := { z | -f z ∈ Complex.slitPlane} ∩ s have h₁' : DifferentiableOn ℂ (-f) s := by rw [← differentiableOn_neg_iff] simp exact h₁ have hs₂ : IsOpen s₂ := by let A := DifferentiableOn.continuousOn h₁' let B := continuousOn_iff'.1 A obtain ⟨u, hu₁, hu₂⟩ := B Complex.slitPlane Complex.isOpen_slitPlane have : u ∩ s = s₂ := by rw [← hu₂] tauto rw [← this] apply IsOpen.inter hu₁ hs have harm₂ : HarmonicOn (Real.log ∘ Complex.normSq ∘ (-f)) s₂ := by apply log_normSq_of_holomorphicOn_is_harmonicOn' exact hs₂ apply DifferentiableOn.mono h₁' (Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s) -- ∀ z ∈ s₁, f z ≠ 0 intro z hz simp exact h₂ z (Set.mem_of_mem_inter_right hz) -- ∀ z ∈ s₁, f z ∈ Complex.slitPlane intro z hz apply hz.1 apply HarmonicOn_of_locally_HarmonicOn intro z hz by_cases hfz : f z ∈ Complex.slitPlane · use s₁ constructor · exact hs₁ · constructor · tauto · have : s₁ = s ∩ s₁ := by apply Set.right_eq_inter.mpr exact Set.inter_subset_right {z | f z ∈ Complex.slitPlane} s rw [← this] exact harm₁ · use s₂ constructor · exact hs₂ · constructor · constructor · apply Or.resolve_left (slitPlaneLemma (h₂ z hz)) hfz · exact hz · have : s₂ = s ∩ s₂ := by apply Set.right_eq_inter.mpr exact Set.inter_subset_right {z | -f z ∈ Complex.slitPlane} s rw [← this] have : Real.log ∘ ⇑Complex.normSq ∘ f = Real.log ∘ ⇑Complex.normSq ∘ (-f) := by funext x simp rw [this] exact harm₂ 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₃