From bb2732106c4ee9d7cbe8b9e46e48c3c48220e0dc Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 16 May 2024 09:19:45 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 36 ++++++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 9 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 536a415..7be3c94 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -126,6 +126,13 @@ theorem logabs_of_holomorphic_is_harmonic have f_is_real_C2 : ContDiff ℝ 2 f := ContDiff.restrict_scalars ℝ (Differentiable.contDiff h₁) + -- Complex.log ∘ f is real C² + have t₀ : Differentiable ℂ (Complex.log ∘ f) := by + intro z + apply DifferentiableAt.comp + exact Complex.differentiableAt_log (h₃ z) + exact h₁ z + -- The norm square is z * z.conj have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul' @@ -231,14 +238,8 @@ theorem logabs_of_holomorphic_is_harmonic rw [this] rw [laplace_add] - have : Differentiable ℂ (Complex.log ∘ f) := by - intro z - apply DifferentiableAt.comp - exact Complex.differentiableAt_log (h₃ z) - exact h₁ z - have t₁: Complex.laplace (Complex.log ∘ f) = 0 := by - let A := holomorphic_is_harmonic this + let A := holomorphic_is_harmonic t₀ funext z exact A.2 z rw [t₁] @@ -257,6 +258,23 @@ theorem logabs_of_holomorphic_is_harmonic rw [laplace_compCLE] rw [t₁] simp + + -- ContDiff ℝ 2 (Complex.log ∘ f) + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀) + + -- ContDiff ℝ 2 (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) + sorry - sorry - sorry + + -- ContDiff ℝ 2 (Complex.log ∘ f) + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff t₀) + + -- ContDiff ℝ 2 (Real.log ∘ ⇑Complex.normSq ∘ f) + 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