From 2d7e62bb49964d26fcce019d6bf5128ec0e42a2b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 18 Jun 2024 09:56:44 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 62 +++++++++++++++++++++------
 1 file changed, 48 insertions(+), 14 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 0050ff7..c18e1af 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -243,14 +243,38 @@ theorem primitive_fderivAtBasepoint
         let A := mem_ball_iff_norm.1 hy
         simp at A
         assumption
+    have h₂y : |y.im| < ε := by
+      calc |y.im|
+      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
+      _ < ε := by
+        let A := mem_ball_iff_norm.1 hy
+        simp at A
+        assumption
+
+    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
+      let A := h.1
+      let B := h.2
+      rcases le_total 0 y' with hy | hy
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonneg hy]
+        rw [abs_of_nonneg (le_of_lt A)]
+        exact B
+      · simp [hy] at A
+        simp [hy] at B
+        rw [abs_of_nonpos hy]
+        rw [abs_of_nonpos]
+        linarith [h.1]
+        exact B
 
     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
+        calc |x|
+          _ ≤ |y.re| := intervalComputation hx
+          _ < ε := h₁y
       apply le_of_lt
       apply h₃ε { re := x, im := 0 }
       rw [mem_ball_iff_norm]
@@ -264,16 +288,21 @@ theorem primitive_fderivAtBasepoint
     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
+        calc |x|
+          _ ≤ |y.im| := intervalComputation hx
+          _ < ε := h₂y
+
       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 Complex.abs { re := y.re, im := x }
+        _ ≤ |y.re| + |x| := by
+          apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
+        _ ≤ 2 * ε := by
+          linarith
 
     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
@@ -282,14 +311,19 @@ theorem primitive_fderivAtBasepoint
         simp
         rw [norm_smul]
         simp
-      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
+      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
         apply add_le_add
         exact t₁
-        rfl
-      _ ≤ c * ‖y‖ := by sorry
-
-
-  sorry
+        exact t₂
+      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
+        simp
+        rw [mul_add]
+      _ ≤ c * ‖y‖ := by
+        apply mul_le_mul
+        apply div_le_self
+        exact le_of_lt hc
+        linarith
+        sorry
 
 
 theorem primitive_additivity