From 46ededdde7c54f6bde6bd070af1aa3c41d13fe76 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 17 Jun 2024 17:22:17 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 54 +++++++++++++++++++--------
 1 file changed, 38 insertions(+), 16 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index c1c40ef..0050ff7 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -219,52 +219,74 @@ theorem primitive_fderivAtBasepoint
     rw [← intervalIntegral.integral_sub t₂ t₃]
   rw [Filter.eventually_iff_exists_mem]
 
-  let s := f⁻¹' Metric.ball (f 0) c
+  let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ))
   have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
   have h₂s : 0 ∈ s := by
     apply Set.mem_preimage.mpr
-    exact Metric.mem_ball_self hc
+    apply Metric.mem_ball_self
+    linarith
 
   obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
 
-  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < c := by
+  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
     intro y hy
-    exact mem_ball_iff_norm.mp (h₂ε hy)
+    apply mem_ball_iff_norm.mp (h₂ε hy)
 
   use Metric.ball 0 ε
   constructor
   · exact Metric.ball_mem_nhds 0 h₁ε
   · intro y hy
     have h₁y : |y.re| < ε := by
+      calc |y.re|
+      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
+      _ < ε := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        assumption
 
-      sorry
-
-    have : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ c * |y.re - 0| := by
+    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
       apply intervalIntegral.norm_integral_le_of_norm_le_const
       intro x hx
-      have h₁x : |x| < ε := by sorry
+
+      have h₁x : |x| < ε := by
+
+        sorry
       apply le_of_lt
       apply h₃ε { re := x, im := 0 }
+      rw [mem_ball_iff_norm]
       simp
       have : { re := x, im := 0 } = (x : ℂ) := by rfl
       rw [this]
       rw [Complex.abs_ofReal]
       exact h₁x
 
-    sorry
-    /-
+
+    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+      have h₁x : |x| < ε := by
+        sorry
+      apply le_of_lt
+      apply h₃ε { re := y.re, im := x }
+      simp
+      have : { re := y.re, im := x } = (x : ℂ) := by
+        rfl
+      rw [this]
+      rw [Complex.abs_ofReal]
+      exact h₁x
+
     calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by apply norm_add_le
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+        apply norm_add_le
       _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
         simp
         rw [norm_smul]
         simp
-      _ ≤ |(∫ (x : ℝ) in (0)..(y.re), ‖f { re := x, im := 0 } - f 0‖)| + |∫ (x : ℝ) in (0)..(y.im), ‖f { re := y.re, im := x } - f 0‖| := by
+      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
         apply add_le_add
-        apply intervalIntegral.norm_integral_le_abs_integral_norm
-        apply intervalIntegral.norm_integral_le_abs_integral_norm
-      _ ≤
-    -/
+        exact t₁
+        rfl
+      _ ≤ c * ‖y‖ := by sorry
 
 
   sorry