From 06f8de2f56d7380ff9281ef1dbedadb4c9e33425 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 14 May 2024 17:02:45 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 9961396..5a3f612 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -128,13 +128,20 @@ theorem logabs_of_holomorphic_is_harmonic 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 - sorry + apply ContinuousLinearMap.contDiff Complex.reCLM + apply ContinuousLinearMap.contDiff Complex.reCLM + apply ContDiff.mul + apply ContinuousLinearMap.contDiff Complex.imCLM + apply ContinuousLinearMap.contDiff Complex.imCLM constructor · -- logabs f is real C² - have : (fun z ↦ Real.log ‖f z‖) = (Real.log ∘ Complex.normSq ∘ f) / 2 := by funext z simp @@ -143,8 +150,10 @@ theorem logabs_of_holomorphic_is_harmonic rw [Real.log_sqrt] 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 - sorry + have : Real.log ∘ ⇑Complex.normSq ∘ f / 2 = (fun z ↦ (1 / (2 : ℝ)) • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by + funext z + simp + exact div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2 rw [this] apply contDiff_iff_contDiffAt.2 @@ -160,4 +169,5 @@ theorem logabs_of_holomorphic_is_harmonic exact ContDiff.contDiffAt f_is_real_C2 · -- Laplace vanishes + sorry