From 71ad6aa67ec7afe25b43532c2493330f2e69ee97 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 16 May 2024 21:46:01 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 212 ++++++++++++++++++++++++++++---- 1 file changed, 190 insertions(+), 22 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 28da225..4977809 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -17,13 +17,47 @@ 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) -theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : +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 ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) + · rw [laplace_compContLin] + simp + intro z + rw [h.2 z] + simp + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) + + +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 holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) : Harmonic f := by -- f is real C² @@ -83,36 +117,170 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : exact fI_is_real_differentiable -theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : +theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : Harmonic (Complex.reCLM ∘ f) := by - - constructor - · -- Continuous differentiability - apply ContDiff.comp - exact ContinuousLinearMap.contDiff Complex.reCLM - exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) - · rw [laplace_compContLin] - simp - intro z - rw [(holomorphic_is_harmonic h).right z] - simp - exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) + apply harmonic_comp_CLM_is_harmonic + exact holomorphic_is_harmonic h -theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : +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 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 + + + + /- We start with a number of lemmas on regularity of all the functions involved -/ + + -- The norm square is real C² + have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by + unfold Complex.normSq + simp + conv => + arg 3 + intro x + rw [← Complex.reCLM_apply, ← Complex.imCLM_apply] + apply ContDiff.add + apply ContDiff.mul + apply ContinuousLinearMap.contDiff Complex.reCLM + apply ContinuousLinearMap.contDiff Complex.reCLM + apply ContDiff.mul + apply ContinuousLinearMap.contDiff Complex.imCLM + apply ContinuousLinearMap.contDiff Complex.imCLM + + -- f is real C² + have f_is_real_C2 : ContDiff ℝ 2 f := + ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁) + + -- Complex.log ∘ f is real C² + have log_f_is_holomorphic : Differentiable ℂ (Complex.log ∘ f) := by + intro z + apply DifferentiableAt.comp + exact Complex.differentiableAt_log (h₃ z) + exact h₁ z + + -- Real.log |f|² is real C² + have t₄ : ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) := by + rw [contDiff_iff_contDiffAt] + intro z + apply ContDiffAt.comp + apply Real.contDiffAt_log.mpr + simp + exact h₂ z + apply ContDiff.comp_contDiffAt z normSq_is_real_C2 + exact ContDiff.contDiffAt f_is_real_C2 + + have t₂ : 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) constructor - · -- Continuous differentiability - apply ContDiff.comp - exact ContinuousLinearMap.contDiff Complex.imCLM - exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) - · rw [laplace_compContLin] + · -- logabs f is real C² + 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] + + have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by + exact rfl + rw [this] + apply ContDiff.const_smul + exact t₄ + + · -- Laplace vanishes + 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] + rw [laplace_smul] simp + + have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by + intro z + rw [laplace_compContLin] + simp + -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) + exact t₄ + conv => + intro z + rw [this z] + + have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by + unfold Function.comp + funext z + apply Complex.ofReal_log + exact Complex.normSq_nonneg (f z) + rw [this] + + have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by + funext z + simp + exact Complex.normSq_eq_conj_mul_self + rw [this] + + 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] + rw [laplace_add] + + rw [t₂, laplace_compCLE] intro z - rw [(holomorphic_is_harmonic h).right z] simp - exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) + rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z] + simp + + -- ContDiff ℝ 2 (Complex.log ∘ f) + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic) + + -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) + rw [t₂] + apply ContDiff.comp + exact ContinuousLinearEquiv.contDiff Complex.conjCLE + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic) + + -- ContDiff ℝ 2 (Complex.log ∘ f) + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic) + + -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) + exact t₄ theorem logabs_of_holomorphic_is_harmonic