From ac3cd65bf201f49b26fabfe77fd2540a3294a578 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 30 May 2024 10:49:16 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 577b52d..8038f53 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -220,16 +220,16 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn -- 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 + have : ∀ z ∈ s, (Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f)) z = (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f) z := by + intro z hz 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) + exact Complex.slitPlane_arg_ne_pi (h₃ z hz) simp tauto rw [this] @@ -237,8 +237,9 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn constructor · exact Real.pi_pos · exact Real.pi_nonneg - exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z) - exact h₂ z + exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z hz) + exact h₂ z hz + rw [this] apply harmonic_add_harmonic_is_harmonic