From f239759275b358c982b9aba0fdc836ad9e405581 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 2 May 2024 17:55:26 +0200 Subject: [PATCH] Update complexHarmonic.lean --- Nevanlinna/complexHarmonic.lean | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index 828a180..05d0ae1 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -17,18 +17,6 @@ noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by def Harmonic (f : ℂ → ℝ) : Prop := (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0) -#check contDiff_iff_ftaylorSeries.2 - -lemma c2_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℂ 2 f := by - intro fHyp - exact Differentiable.contDiff fHyp - -lemma c2R_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℝ 2 f := by - intro fHyp - let ZZ := c2_if_holomorphic f fHyp - apply ContDiff.restrict_scalars ℝ ZZ - - theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) : Differentiable ℂ f → Harmonic (Complex.reCLM ∘ f) := by @@ -41,7 +29,7 @@ theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) : · -- Complex.reCLM is two times real continuously differentiable exact ContinuousLinearMap.contDiff Complex.reCLM · -- f is two times real continuously differentiable - exact c2R_if_holomorphic f h + exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h) · -- Laplace of f is zero intro z