From e76e9abaf39f2b2ea15c43768c6a7ffe591d582c Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 3 Jun 2024 13:59:10 +0200 Subject: [PATCH] split off file --- Nevanlinna/complexHarmonic.examples.lean | 325 +++++++++++++++++++++++ Nevanlinna/complexHarmonic.lean | 303 --------------------- 2 files changed, 325 insertions(+), 303 deletions(-) create mode 100644 Nevanlinna/complexHarmonic.examples.lean diff --git a/Nevanlinna/complexHarmonic.examples.lean b/Nevanlinna/complexHarmonic.examples.lean new file mode 100644 index 0000000..07935cb --- /dev/null +++ b/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₃ diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 26d7482..1994f11 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/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₃