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.partialDeriv 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₁] 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 HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) : HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by constructor · intro h₁ constructor · apply ContDiffOn.congr h₁.1 intro x hx rw [eq_comm] exact hf₁₂ x hx · intro z hz have : f₁ =ᶠ[nhds z] f₂ := by unfold Filter.EventuallyEq unfold Filter.Eventually simp refine mem_nhds_iff.mpr ?_ use s constructor · exact hf₁₂ · constructor · exact hs · exact hz rw [← laplace_eventuallyEq this] exact h₁.2 z hz · intro h₁ constructor · apply ContDiffOn.congr h₁.1 intro x hx exact hf₁₂ x hx · intro z hz have : f₁ =ᶠ[nhds z] f₂ := by unfold Filter.EventuallyEq unfold Filter.Eventually simp refine mem_nhds_iff.mpr ?_ use s constructor · exact hf₁₂ · constructor · exact hs · exact hz rw [laplace_eventuallyEq this] exact h₁.2 z hz theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) : Harmonic (f₁ + f₂) := by constructor · exact ContDiff.add h₁.1 h₂.1 · rw [laplace_add h₁.1 h₂.1] simp intro z rw [h₁.2 z, h₂.2 z] simp theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) : HarmonicOn (f₁ + f₂) s := by constructor · exact ContDiffOn.add h₁.1 h₂.1 · intro z hz rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz] rw [h₁.2 z hz, h₂.2 z hz] simp theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) : Harmonic (c • f) := by constructor · exact ContDiff.const_smul c h.1 · rw [laplace_smul] dsimp intro z rw [h.2 z] simp theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) : Harmonic f ↔ Harmonic (c • f) := by constructor · exact harmonic_smul_const_is_harmonic · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)] exact fun a => harmonic_smul_const_is_harmonic a theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) : Harmonic (l ∘ f) := by constructor · -- Continuous differentiability apply ContDiff.comp exact ContinuousLinearMap.contDiff l exact h.1 · rw [laplace_compContLin] simp intro z rw [h.2 z] simp exact ContDiff.restrict_scalars ℝ h.1 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 · -- Continuous differentiability apply ContDiffOn.continuousLinearMap_comp exact h.1 · -- Vanishing of Laplace 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₁} : Harmonic f ↔ Harmonic (l ∘ f) := by constructor · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl rw [this] exact harmonic_comp_CLM_is_harmonic · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by funext z unfold Function.comp simp nth_rewrite 2 [this] exact harmonic_comp_CLM_is_harmonic theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ ≃L[ℝ] G₁} (hs : IsOpen s) : HarmonicOn f s ↔ HarmonicOn (l ∘ f) s := by constructor · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl rw [this] exact harmonicOn_comp_CLM_is_harmonicOn hs · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by funext z unfold Function.comp 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 apply? exact h₁ z 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₃