Update holomorphic.primitive.lean

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 t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
-
-    have : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ c * |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
+        exact t₁
-        apply intervalIntegral.norm_integral_le_abs_integral_norm
+        rfl
-      _ ≤
+      _ ≤ c * ‖y‖ := by sorry
-    -/
 
 
   sorry