From fcbdd1a2c2c22de0d73ae39743e5be253fca4a8c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 14 Jun 2024 16:07:58 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 64 +++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 579130a..137e34a 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -131,3 +131,67 @@ theorem integral_divergence₅
     rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B
   simp at B
   exact B
+
+
+noncomputable def primitive
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
+  ℂ  → (ℂ → E) → (ℂ → E) := by
+  intro z₀
+  intro f
+  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
+
+
+theorem primitive_zeroAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E)
+  (z₀ : ℂ) :
+  (primitive z₀ f) z₀ = 0 := by
+  unfold primitive
+  simp
+
+
+theorem primitive_lem1
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
+  (v : E) :
+  HasDerivAt (primitive 0 (fun z ↦ v)) v 0 := by
+  unfold primitive
+  simp
+
+  have : (fun (z : ℂ) => z.re • v + Complex.I • z.im • v) = (fun (z : ℂ) => z • 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]
+
+
+  apply HasDerivAt.smul_const
+
+
+
+  sorry
+
+
+
+theorem primitive_fderivAtBasepoint
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  (f : ℂ  → E) :
+  HasDerivAt (primitive 0 f) (f 0) 0 := by
+  unfold primitive
+  simp
+
+  sorry
+
+
+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
+
+
+  sorry