working

Nevanlinna/holomorphic_primitive2.lean

@@ -289,47 +289,6 @@ theorem primitive_hasDerivAtBasepoint
   exact hasDerivAt_id z₀
 
 
-lemma integrability₁
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (a₁ a₂ b : ℝ) :
-  IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
-  apply Continuous.intervalIntegrable
-  apply Continuous.comp
-  exact Differentiable.continuous hf
-  have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-    funext x
-    apply Complex.ext
-    rw [Complex.add_re]
-    simp
-    rw [Complex.add_im]
-    simp
-  rw [this]
-  continuity
-
-
-lemma integrability₂
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f)
-  (a₁ a₂ b : ℝ) :
-  IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by
-  apply Continuous.intervalIntegrable
-  apply Continuous.comp
-  exact Differentiable.continuous hf
-  have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
-    funext x
-    apply Complex.ext
-    rw [Complex.add_re]
-    simp
-    simp
-  rw [this]
-  apply Continuous.add
-  continuity
-  fun_prop
-
-
 theorem primitive_additivity
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
@@ -545,8 +504,40 @@ theorem primitive_additivity'
   (hz₁ : z₁ ∈ Metric.ball z₀ R)
   :
   primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
+
+  let ε := R - dist z₀ z₁
+  let rx := dist z₀.re z₁.re + ε/(2 : ℝ)
+  let ry := dist z₀.im z₁.im + ε/(2 : ℝ)
+
+  have h'ry : 0 < ry := by
     sorry
 
+  have h'f : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
+    sorry
+
+  have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
+    sorry
+
+  let A := primitive_additivity f z₀ rx ry h'ry h'f z₁ h'z₁
+  obtain ⟨εx, εy, hε⟩ := A
+
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy)
+  constructor
+  · apply IsOpen.mem_nhds
+    apply IsOpen.reProdIm
+    exact Metric.isOpen_ball
+    exact Metric.isOpen_ball
+    constructor
+    · simp
+      sorry
+    · simp
+      sorry
+  · intro x hx
+    simp
+    rw [← sub_zero (primitive z₀ f x), ← hε x hx]
+    abel
+
 
 theorem primitive_hasDerivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]