From fc3a4ae3f34e8bfe485929e43951c85bb9fc0a01 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 7 Aug 2024 13:11:53 +0200
Subject: [PATCH] Update holomorphic_primitive2.lean

---
 Nevanlinna/holomorphic_primitive2.lean | 40 ++++++++++++++++++++++----
 1 file changed, 34 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index a26590d..3447e8a 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -22,6 +22,7 @@ theorem primitive_fderivAtBasepointZero
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
   {R : ℝ}
+  (hR : 0 < R)
   (hf : ContinuousOn f (Metric.ball 0 R)) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
@@ -48,6 +49,7 @@ theorem primitive_fderivAtBasepointZero
     rw [this]
   have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
     abel
+
   have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
     apply Continuous.intervalIntegrable
     apply Continuous.comp
@@ -55,6 +57,7 @@ theorem primitive_fderivAtBasepointZero
     have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
     rw [this]
     continuity
+
   have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
     apply Continuous.intervalIntegrable
     apply Continuous.comp
@@ -97,11 +100,17 @@ theorem primitive_fderivAtBasepointZero
     exact eventually_nhds_iff.mp (continuousAt_def.1 hf (Metric.ball (f 0) (c / (4 : ℝ))) B)
 
   obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s := by
-    obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s := by
+    obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
       apply Metric.mem_nhds_iff.mp
       apply IsOpen.mem_nhds
+      apply IsOpen.inter
       exact h₂s.1
-      exact h₂s.2
+      exact Metric.isOpen_ball
+      constructor
+      · exact h₂s.2
+      · simp
+
+        sorry
     use (2 : ℝ)⁻¹ * ε'
     constructor
     · simpa
@@ -280,6 +289,7 @@ theorem primitive_hasDerivAtBasepoint
   {f : ℂ  → E}
   {R : ℝ}
   (z₀ : ℂ)
+  (hR : 0 < R)
   (hf : ContinuousOn f (Metric.ball z₀ R)) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
@@ -310,7 +320,7 @@ theorem primitive_hasDerivAtBasepoint
   simp
   have : g 0 = f z₀ := by simp [g]
   rw [← this]
-  exact primitive_fderivAtBasepointZero hg
+  exact primitive_fderivAtBasepointZero hR hg
   apply HasDerivAt.sub_const
   have : (fun (x : ℂ) ↦ x) = id := by
     funext x
@@ -670,13 +680,31 @@ theorem primitive_hasDerivAt
   rw [Filter.EventuallyEq.hasDerivAt_iff A]
   rw [← add_zero (f z)]
   apply HasDerivAt.add
-  apply primitive_hasDerivAtBasepoint
 
-  apply hf.continuousOn.continuousAt
-  apply (IsOpen.mem_nhds_iff Metric.isOpen_ball).2 hz
+  let R' := R - dist z z₀
+  have h₀R' : 0 < R' := by
+    dsimp [R']
+    simp
+    exact hz
+  have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by
+    intro x hx
+    simp
+    calc dist x z₀
+    _ ≤ dist x z + dist z z₀ := dist_triangle x z z₀
+    _ < R' + dist z z₀ := by
+      refine add_lt_add_right ?bc (dist z z₀)
+      exact hx
+    _ = R := by
+      dsimp [R']
+      simp
+
+  apply primitive_hasDerivAtBasepoint
+  exact h₀R'
+  apply ContinuousOn.mono hf.continuousOn h₁R'
   apply hasDerivAt_const
 
 
+
 theorem primitive_differentiable
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}