Update holomorphic.primitive.lean

Nevanlinna/holomorphic.primitive.lean

@@ -1,7 +1,10 @@
 import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
+
+
 import Nevanlinna.cauchyRiemann
 import Nevanlinna.partialDeriv
 
@@ -95,7 +98,7 @@ theorem integral_divergence₅
   (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩)  + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ =
   (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re,  x⟩ := by
 
-  let h₁f : ContDiff ℝ 1 F :=  (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ
+  let h₁f : ContDiff ℝ 1 F := (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ
 
   let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by
     have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl
@@ -151,30 +154,6 @@ theorem primitive_zeroAtBasepoint
   simp
 
 
-theorem primitive_lem1
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
-  (v : E) :
-  HasDerivAt (primitive 0 (fun _ ↦ v)) v 0 := by
-  unfold primitive
-  simp
-
-  have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (y : ℂ) => ((fun w ↦ w)  y) • v) := by
-    funext z
-    rw [smul_comm]
-    rw [← smul_assoc]
-    simp
-    have : z.re • v = (z.re : ℂ) • v := by exact rfl
-    rw [this, ← add_smul]
-    simp
-  rw [this]
-
-  have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by
-    apply hasDerivAt_id'
-  nth_rewrite 2 [← (one_smul ℂ v)]
-  exact HasDerivAt.smul_const hc v
-
-
-
 theorem primitive_fderivAtBasepointZero
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
@@ -380,12 +359,122 @@ theorem primitive_fderivAtBasepointZero
         linarith
 
 
+theorem primitive_translation
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ t : ℂ) :
+  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
+  funext z
+  unfold primitive
+  simp
+
+  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
+  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
+  simp
+
+  congr 1
+  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
+  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
+    congr 1
+    apply Complex.ext <;> simp
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
+  simp
+
+
+theorem primitive_fderivAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {z₀ : ℂ}
+  (f : ℂ  → E)
+  (hf : Continuous f) :
+  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
+
+  let g := f ∘ fun z ↦ z + z₀
+  have : Continuous g := by continuity
+  let A := primitive_fderivAtBasepointZero g this
+  simp at A
+
+  let B := primitive_translation g z₀ z₀
+  simp at B
+  have : (g ∘ fun z ↦ (z - z₀)) = f := by
+    funext z
+    dsimp [g]
+    simp
+  rw [this] at B
+  rw [B]
+  have : f z₀ = (1 : ℂ) • (f z₀) := by
+    exact (MulAction.one_smul (f z₀)).symm
+  conv =>
+    arg 2
+    rw [this]
+
+  apply HasDerivAt.scomp
+  simp
+  have : g 0 = f z₀ := by simp [g]
+  rw [← this]
+  exact A
+  apply HasDerivAt.sub_const
+  have : (fun (x : ℂ) ↦ x) = id := by
+    funext x
+    simp
+  rw [this]
+  exact hasDerivAt_id z₀
+
+
 theorem primitive_additivity
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
   (hf : Differentiable ℂ f)
   (z₀ z₁ : ℂ) :
-  (primitive z₁ f) = (primitive z₀ f) - (fun z ↦ primitive z₀ f z₁) := by
+  primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
+  funext 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 Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact Differentiable.continuous hf
+    sorry
+    --
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
+    exact Differentiable.continuous hf
+    sorry
+  rw [this]
 
-  sorry
+  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
+  rw [this]
+  simp
+
+  let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩
+  simp at A
+
+  have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by
+    abel
+  rw [this]
+  rw [A]
+  abel