working

Nevanlinna/holomorphic_primitive2.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.Complex.TaylorSeries
-
+import Mathlib.Data.ENNReal.Basic
 
 noncomputable def primitive
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
@@ -333,23 +333,24 @@ lemma integrability₂
 theorem primitive_additivity
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (z₀ z₁ : ℂ) :
-  (fun z ↦ (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁)) = 0 := by
-  funext z
-
-
+  (z₀ : ℂ)
+  (R : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  (z₁ : ℂ)
+  (hz₁ : z₁ ∈ Metric.ball z₀ R) :
+  ∀ z ∈ Metric.ball z₁ (R - ‖z₁‖), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
+  intro z _
 
   unfold primitive
   have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
     rw [intervalIntegral.integral_add_adjacent_intervals]
-    apply integrability₁ f hf
-    apply integrability₁ f hf
+    sorry --apply integrability₁ f hf
+    sorry --apply integrability₁ f hf
   rw [this]
   have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
     rw [intervalIntegral.integral_add_adjacent_intervals]
-    apply integrability₂ f hf
-    apply integrability₂ f hf
+    sorry --apply integrability₂ f hf
+    sorry --apply integrability₂ f hf
   rw [this]
   simp
 
@@ -358,7 +359,14 @@ theorem primitive_additivity
   rw [this]
   simp
 
-  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ (hf.differentiableOn)
+  have H : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
+    apply DifferentiableOn.mono hf
+    intro x hx
+    simp
+
+    sorry
+
+  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H
   have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
     apply Complex.ext
     · simp