From dd207b19a2a354420ce0434cf726730a29d33dcf Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 16:45:26 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_examples.lean  | 28 ++++------
 Nevanlinna/holomorphic_primitive.lean | 73 +++++++++++++++++++++++----
 2 files changed, 75 insertions(+), 26 deletions(-)

diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index 54648c3..769dee6 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -194,28 +194,20 @@ theorem harmonic_is_realOfHolomorphic
       exact reg₁f_I.differentiable le_rfl
   
   let F := fun z ↦ (primitive 0 g) z + f 0
+
   have regF : Differentiable ℂ F := by 
     apply Differentiable.add
-    intro x
-    let A : HasDerivAt (primitive 0 g) (g x) x := primitive_fderiv g reg₁
-    exact A.differentiableAt 
+    apply primitive_differentiable reg₁
     simp
 
-  have pF' : ∀ x, (fderiv ℂ F x) = ContinuousLinearMap.lsmul ℂ ℂ (g x) := by 
-    intro x
-    dsimp [F]
-    rw [fderiv_add_const]
-    let A : HasDerivAt (primitive 0 g) (g x) x := primitive_fderiv g reg₁
-    let B : HasFDerivAt (primitive 0 g) (ContinuousLinearMap.lsmul ℂ ℂ (g x)) x := by
-      rw [hasFDerivAt_iff_hasDerivAt]
-      simp
-      exact A
-    exact HasFDerivAt.fderiv B
-
   have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by 
     intro x
-    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x), pF' x]
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x)]
+    dsimp [F]
+    rw [fderiv_add_const]
+    rw [primitive_fderiv']
     exact rfl
+    exact reg₁
 
   use F
   intro z
@@ -241,6 +233,7 @@ theorem harmonic_is_realOfHolomorphic
       simp
 
     apply eq_of_fderiv_eq B A _ 0 C
+
     intro x
     rw [fderiv.comp]
     simp
@@ -257,6 +250,7 @@ theorem harmonic_is_realOfHolomorphic
     rw [smul_eq_mul, smul_eq_mul]
     ring
     -- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
-    exact ContinuousLinearMap.differentiableAt Complex.reCLM
-    -- DifferentiableAt ℝ F x
+    fun_prop
+    -- DifferentiableAt ℝ F x    
     exact regF.restrictScalars ℝ x
+
diff --git a/Nevanlinna/holomorphic_primitive.lean b/Nevanlinna/holomorphic_primitive.lean
index 4e7a4de..9b393cc 100644
--- a/Nevanlinna/holomorphic_primitive.lean
+++ b/Nevanlinna/holomorphic_primitive.lean
@@ -485,11 +485,11 @@ theorem primitive_translation
   simp
 
 
-theorem primitive_fderivAtBasepoint
+theorem primitive_hasDerivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {z₀ : ℂ}
-  (f : ℂ  → E)
-  (hf : Continuous f) :
+  {f : ℂ  → E}
+  (hf : Continuous f)   
+  (z₀ : ℂ) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
@@ -597,15 +597,70 @@ theorem primitive_additivity
   abel
 
 
-theorem primitive_fderiv
+theorem primitive_hasDerivAt
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {z₀ z : ℂ}
-  (f : ℂ  → E)
-  (hf : Differentiable ℂ f) :
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ z : ℂ) :
   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
+  apply primitive_hasDerivAtBasepoint
   exact hf.continuous
   apply hasDerivAt_const
+
+
+theorem primitive_differentiable
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  Differentiable ℂ (primitive z₀ f) := by
+  intro z
+  exact (primitive_hasDerivAt hf z₀ z).differentiableAt 
+
+
+theorem primitive_hasFderivAt
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
+  intro z
+  rw [hasFDerivAt_iff_hasDerivAt]
+  simp    
+  exact primitive_hasDerivAt hf z₀ z
+
+
+theorem primitive_hasFderivAt'
+  {f : ℂ  → ℂ}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
+  intro z
+  rw [hasFDerivAt_iff_hasDerivAt]
+  simp    
+  exact primitive_hasDerivAt hf z₀ z
+
+
+theorem primitive_fderiv
+  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
+  {f : ℂ  → E}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
+  intro z
+  apply HasFDerivAt.fderiv
+  exact primitive_hasFderivAt hf z₀ z
+
+
+theorem primitive_fderiv'
+  {f : ℂ  → ℂ}
+  (hf : Differentiable ℂ f)
+  (z₀ : ℂ) :
+  ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
+  intro z
+  apply HasFDerivAt.fderiv
+  exact primitive_hasFderivAt' hf z₀ z
+