diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index eca98e5..6537af8 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -26,7 +26,7 @@ def Harmonic (f : ℂ → F) : Prop := (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0) -theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F₁} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) : +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 @@ -37,6 +37,25 @@ theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F₁} (h₁ : Har 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 h.1] + 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 @@ -149,31 +168,17 @@ theorem log_normSq_of_holomorphic_is_harmonic (h₃ : ∀ z, f z ∈ Complex.slitPlane) : Harmonic (Real.log ∘ Complex.normSq ∘ f) := by - -- Suffices to show Harmonic (⇑Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) - let F := Real.log ∘ Complex.normSq ∘ f - have : Harmonic (Complex.ofRealCLM ∘ F) → Harmonic F := by - intro hyp - have t₁ : Harmonic (Complex.reCLM ∘ Complex.ofRealCLM ∘ F) := harmonic_comp_CLM_is_harmonic hyp - have t₂ : Complex.reCLM ∘ Complex.ofRealCLM ∘ F = F := rfl - rw [t₂] at t₁ - exact t₁ - apply this - dsimp [F] + 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 to show Harmonic (Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f) - 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] - - -- Suffices to show Harmonic (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) - have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by - funext z - simp - exact Complex.normSq_eq_conj_mul_self - rw [this] + 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) @@ -224,146 +229,18 @@ theorem logabs_of_holomorphic_is_harmonic (h₃ : ∀ z, f z ∈ Complex.slitPlane) : Harmonic (fun z ↦ Real.log ‖f z‖) := 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 + -- Suffices: Harmonic (2⁻¹ • Real.log ∘ ⇑Complex.normSq ∘ f) + have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by funext z - unfold Function.comp - rw [Complex.log_conj] - rfl - exact Complex.slitPlane_arg_ne_pi (h₃ z) - - constructor - · -- 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 - simp - rw [(holomorphic_is_harmonic log_f_is_holomorphic).2 z] + 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] - -- ContDiff ℝ 2 (Complex.log ∘ f) - exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff log_f_is_holomorphic) + -- Suffices: Harmonic (Real.log ∘ ⇑Complex.normSq ∘ f) + apply (harmonic_iff_smul_const_is_harmonic (inv_ne_zero two_ne_zero)).1 - -- 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₄ + exact log_normSq_of_holomorphic_is_harmonic h₁ h₂ h₃