From 7a281ff514273044912b9781f9b7547eec20ca58 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 19 Jun 2024 08:20:36 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/cauchyRiemann.lean | 6 ++++-- Nevanlinna/holomorphic.primitive.lean | 3 --- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean index 243ad35..1884075 100644 --- a/Nevanlinna/cauchyRiemann.lean +++ b/Nevanlinna/cauchyRiemann.lean @@ -44,8 +44,10 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) simp -theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f) - → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by +theorem CauchyRiemann₄ + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : ℂ → F} : + (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by intro h unfold partialDeriv diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean index 0ac5eae..591d91f 100644 --- a/Nevanlinna/holomorphic.primitive.lean +++ b/Nevanlinna/holomorphic.primitive.lean @@ -4,9 +4,7 @@ import Mathlib.MeasureTheory.Integral.DivergenceTheorem import Mathlib.MeasureTheory.Integral.IntervalIntegral import Mathlib.MeasureTheory.Function.LocallyIntegrable - import Nevanlinna.cauchyRiemann -import Nevanlinna.partialDeriv theorem MeasureTheory.integral2_divergence₃ @@ -108,7 +106,6 @@ theorem integral_divergence₅ exact h₁f let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im - have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl conv at A in (fderiv ℝ F _) _ => rw [this] have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl