From a60e07e602604b37a795073601c9229ed8113fb7 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 14 May 2024 17:24:34 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 5a3f612..da7ec8b 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -142,18 +142,18 @@ theorem logabs_of_holomorphic_is_harmonic constructor · -- logabs f is real C² - have : (fun z ↦ Real.log ‖f z‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by + 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] - exact Complex.normSq_nonneg (f z) + rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2] + exact Complex.normSq_nonneg (f z) rw [this] - have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / (2 : ℝ)) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by - funext z + + have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by simp - exact div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2 rw [this] apply contDiff_iff_contDiffAt.2 @@ -169,5 +169,5 @@ theorem logabs_of_holomorphic_is_harmonic exact ContDiff.contDiffAt f_is_real_C2 · -- Laplace vanishes - + sorry