Update holomorphic.primitive.lean

Nevanlinna/holomorphic.primitive.lean

@@ -176,13 +176,84 @@ theorem primitive_lem1
 
 theorem primitive_fderivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E) :
+  (f : ℂ  → E) 
+  (hf : Continuous f) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
   simp
   apply hasDerivAt_iff_isLittleO.2
   simp
+  rw [Asymptotics.isLittleO_iff]
+  intro c hc
+
+  have {z : ℂ} {e : E} : z • e = (∫ (x : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (x : ℝ) in (0)..(z.im), e:= by 
+    simp
+    rw [smul_comm]
+    rw [← smul_assoc]
+    simp
+    have : z.re • e = (z.re : ℂ) • e := by exact rfl
+    rw [this, ← add_smul]
+    simp
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    arg 2
+    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 sorry
+  have t₁ {r : ℝ} :IntervalIntegrable (fun x => f 0) MeasureTheory.volume 0 r := by sorry
+  have t₂ {a b : ℝ}: IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by sorry
+  have t₃ {a : ℝ} : IntervalIntegrable (fun x => f 0) MeasureTheory.volume 0 a := by sorry
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    rw [this]
+    rw [← smul_sub]
+    rw [← intervalIntegral.integral_sub t₀ t₁]
+    rw [← intervalIntegral.integral_sub t₂ t₃]
+  rw [Filter.eventually_iff_exists_mem]
+
+  let s := f⁻¹' Metric.ball (f 0) c
+  use s
+  constructor
+  · apply IsOpen.mem_nhds
+    apply IsOpen.preimage hf
+    exact Metric.isOpen_ball
+    apply Set.mem_preimage.mpr 
+    exact Metric.mem_ball_self hc
+  · intro y hy
+    have : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ c * |y.re| := by
+      let A := intervalIntegral.norm_integral_le_of_norm_le_const_ae
+      
+
+      sorry
+
+    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)‖ + ‖∫ (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 
+        apply add_le_add
+        apply intervalIntegral.norm_integral_le_abs_integral_norm
+        apply intervalIntegral.norm_integral_le_abs_integral_norm
+      _ ≤ 
+        
+
+
+
   
+
+
+
+
+
   sorry