From 8d100b2333b32ee457cedb7de8e3b74bc4a7e09f Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 15:11:57 +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 | 41 ++++++++++++++++++++--------
 1 file changed, 30 insertions(+), 11 deletions(-)

diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index cdf69a5..54648c3 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -1,4 +1,3 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
 import Nevanlinna.holomorphic_primitive
@@ -194,33 +193,53 @@ theorem harmonic_is_realOfHolomorphic
       apply Differentiable.const_smul
       exact reg₁f_I.differentiable le_rfl
   
-  let F := primitive 0 g
+  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 
+    simp
 
-  have pF : ∀ x a, (fderiv ℝ F x) a = (g x) * a := by 
-    sorry
+  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 regF : Differentiable ℂ F := by sorry
+  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by 
+    intro x
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x), pF' x]
+    exact rfl
 
   use F
   intro z
   constructor
   · -- HolomorphicAt F z
     apply HolomorphicAt_iff.2
-    use {z : ℂ | true}
+    use Set.univ
     constructor
     · exact isOpen_const
     · constructor
       · simp
-      · intro w hw
-        let A : HasDerivAt (primitive 0 g) (g w) w := primitive_fderiv g reg₁
-        apply A.differentiableAt
+      · intro w _
+        exact regF w
   · -- (F z).re = f z
     have A := reg₂f.differentiable one_le_two
     have B : Differentiable ℝ (Complex.reCLM ∘ F) := by 
       apply Differentiable.comp
       exact ContinuousLinearMap.differentiable Complex.reCLM
       exact Differentiable.restrictScalars ℝ regF
-    have C : (F 0).re = f 0 := by sorry
+    have C : (F 0).re = f 0 := by 
+      dsimp [F]
+      rw [primitive_zeroAtBasepoint]
+      simp
+
     apply eq_of_fderiv_eq B A _ 0 C
     intro x
     rw [fderiv.comp]
@@ -228,7 +247,7 @@ theorem harmonic_is_realOfHolomorphic
     apply ContinuousLinearMap.ext
     intro w
     simp
-    rw [pF]
+    rw [pF'']
     dsimp [g, f_1, f_I, partialDeriv]
     simp
     have : w = w.re • 1 + w.im • Complex.I := by simp