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.Defs.Filter import Mathlib.Topology.Instances.RealVectorSpace import Nevanlinna.cauchyRiemann import Nevanlinna.laplace 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] variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace 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 -- 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 rw [HarmonicAt_eventuallyEq this] sorry -- Suffices to show Harmonic (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) -- THIS IS WHERE WE USE h₃ have : (Complex.log ∘ (Complex.conjCLE ∘ f * f)) z = (Complex.log ∘ Complex.conjCLE ∘ f + Complex.log ∘ f) z := by 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 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₃