From 631b1bad70ad7179aa5891da5e5f4e747f76bf71 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 8 May 2024 07:15:34 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 506339a..6ffe7c5 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -39,7 +39,17 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) : · -- Laplace of f is zero unfold Complex.laplace rw [CauchyRiemann₄ h] - rw [partialDeriv_smul₂ fI_is_real_differentiable] + + let l : ℂ →L[ℝ] ℂ := by + -- + sorry --(fun x ↦ Complex.I • x) + have : (Complex.I • Real.partialDeriv 1 f) = (l ∘ (Real.partialDeriv 1 f)) := by + sorry + rw [this] + rw [partialDeriv_compContLin] + + --rw [partialDeriv_smul₂ fI_is_real_differentiable] + rw [partialDeriv_comm f_is_real_C2 Complex.I 1] rw [CauchyRiemann₄ h] rw [partialDeriv_smul₂ fI_is_real_differentiable]