From 50591a54c29eab3310b8f8766bb6f1ac02947cc3 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 18 Jun 2024 19:24:18 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 79 ++++++++++++++++++++-------
 1 file changed, 60 insertions(+), 19 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index f690b9f..0ac5eae 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -434,6 +434,47 @@ theorem primitive_fderivAtBasepoint
   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 : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (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)
@@ -444,29 +485,15 @@ theorem primitive_additivity
   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 Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact Differentiable.continuous hf
-    sorry
-    --
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact Differentiable.continuous hf
-    sorry
+    rw [intervalIntegral.integral_add_adjacent_intervals]   
+    apply integrability₁ f hf 
+    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 Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact Differentiable.continuous hf
-    sorry
-    --
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact Differentiable.continuous hf
-    sorry
+    apply integrability₂ f hf 
+    apply integrability₂ f hf 
   rw [this]
   simp
 
@@ -478,3 +505,17 @@ theorem primitive_additivity
   rw [this]
   rw [A]
   abel
+
+
+theorem primitive_fderiv
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {z₀ z : ℂ}
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f) :
+  HasDerivAt (primitive z₀ f) (f z) z := by
+  rw [primitive_additivity f hf z₀ z]
+  rw [← add_zero (f z)]
+  apply HasDerivAt.add
+  apply primitive_fderivAtBasepoint
+  exact hf.continuous
+  apply hasDerivAt_const