Update holomorphic_primitive2.lean

Nevanlinna/holomorphic_primitive2.lean

@@ -539,24 +539,29 @@ theorem primitive_additivity
 theorem primitive_additivity'
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
+  (z₀ : ℂ)
-  (z₀ z₁ : ℂ) :
+  (R : ℝ)
-  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-
+  (z₁ : ℂ)
-  nth_rw 1 [← sub_zero (primitive z₀ f)]
+  (hz₁ : z₁ ∈ (Metric.ball z₀ R))
-  rw [← primitive_additivity f hf z₀ z₁]
+  :
-
+  ∃ ε : ℝ, ∀ z ∈ (Metric.ball z₁ ε), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
-  funext z
+  sorry
-  simp
-  abel
 
 
 theorem primitive_hasDerivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
+  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
+  (z₀ z : ℂ)
-  (z₀ z : ℂ) :
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  (hz : z ∈ Metric.ball z₀ R) :
   HasDerivAt (primitive z₀ f) (f z) z := by
+
+  let A := primitive_additivity' f z₀ R hf z hz
+
+
+
   rw [primitive_additivity' f hf z₀ z]
   rw [← add_zero (f z)]
   apply HasDerivAt.add