From 6759baea2f3c7fcbd326dcaf486e570c91204f5c Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 5 Aug 2024 12:41:05 +0200 Subject: [PATCH] Update holomorphic_primitive2.lean --- Nevanlinna/holomorphic_primitive2.lean | 31 +++++++++++++++----------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean index d79eb3d..d80b226 100644 --- a/Nevanlinna/holomorphic_primitive2.lean +++ b/Nevanlinna/holomorphic_primitive2.lean @@ -539,24 +539,29 @@ theorem primitive_additivity theorem primitive_additivity' {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → E) - (hf : Differentiable ℂ f) - (z₀ z₁ : ℂ) : - primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by - - nth_rw 1 [← sub_zero (primitive z₀ f)] - rw [← primitive_additivity f hf z₀ z₁] - - funext z - simp - abel + (z₀ : ℂ) + (R : ℝ) + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + (z₁ : ℂ) + (hz₁ : z₁ ∈ (Metric.ball z₀ R)) + : + ∃ ε : ℝ, ∀ z ∈ (Metric.ball z₁ ε), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by + sorry theorem primitive_hasDerivAt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - {f : ℂ → E} - (hf : Differentiable ℂ f) - (z₀ z : ℂ) : + (f : ℂ → E) + (z₀ z : ℂ) + (R : ℝ) + (hf : DifferentiableOn ℂ f (Metric.ball z₀ R)) + (hz : z ∈ Metric.ball z₀ R) : HasDerivAt (primitive z₀ f) (f z) z := by + + let A := primitive_additivity' f z₀ R hf z hz + + + rw [primitive_additivity' f hf z₀ z] rw [← add_zero (f z)] apply HasDerivAt.add