From d4de5d8b5a4b61b2f1e704688c0e470924a7a7cb Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 12:19:59 +0200
Subject: [PATCH] Saving, renaming

---
 ...xamples.lean => holomorphic_examples.lean} | 23 +++++++++++++++----
 ...mitive.lean => holomorphic_primitive.lean} | 13 ++++++-----
 2 files changed, 25 insertions(+), 11 deletions(-)
 rename Nevanlinna/{holomorphic.examples.lean => holomorphic_examples.lean} (93%)
 rename Nevanlinna/{holomorphic.primitive.lean => holomorphic_primitive.lean} (98%)

diff --git a/Nevanlinna/holomorphic.examples.lean b/Nevanlinna/holomorphic_examples.lean
similarity index 93%
rename from Nevanlinna/holomorphic.examples.lean
rename to Nevanlinna/holomorphic_examples.lean
index 26972ee..f4062d2 100644
--- a/Nevanlinna/holomorphic.examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -1,7 +1,7 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Nevanlinna.complexHarmonic
-import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
+import Nevanlinna.holomorphic_primitive
 
 
 theorem CauchyRiemann₆
@@ -194,7 +194,20 @@ theorem harmonic_is_realOfHolomorphic
       apply Differentiable.const_smul
       exact reg₁f_I.differentiable le_rfl
   
-  
-
-
-  sorry
+  let F := primitive 0 g
+  use F
+  intro z
+  constructor
+  · -- HolomorphicAt F z
+    apply HolomorphicAt_iff.2
+    use {z : ℂ | true}
+    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
+  · -- (F z).re = f z
+    
+    sorry
diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic_primitive.lean
similarity index 98%
rename from Nevanlinna/holomorphic.primitive.lean
rename to Nevanlinna/holomorphic_primitive.lean
index c2a67be..4e7a4de 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic_primitive.lean
@@ -3,8 +3,10 @@ import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
+import Nevanlinna.partialDeriv
+import Nevanlinna.cauchyRiemann
 
-
+/-
 noncomputable def partialDeriv
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) :=
@@ -47,7 +49,6 @@ theorem partialDeriv_compCLE
     rw [ContinuousLinearEquiv.comp_differentiableAt_iff]
     exact hyp
 
-
 theorem partialDeriv_smul'₂
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
@@ -84,11 +85,10 @@ theorem partialDeriv_smul'₂
     rw [partialDeriv_compCLE]
     tauto
 
-
 theorem CauchyRiemann₄
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
   {f : ℂ → F} : 
-  (Differentiable ℂ f) → partialDeriv Complex.I f = Complex.I • partialDeriv 1 f := by
+  (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
   unfold partialDeriv
 
@@ -106,6 +106,7 @@ theorem CauchyRiemann₄
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
   funext w
   simp
+-/
 
 
 theorem MeasureTheory.integral2_divergence₃
@@ -207,9 +208,9 @@ theorem integral_divergence₅
     exact h₁f  
 
   let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
-  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv Complex.I F z := by rfl
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ Complex.I F z := by rfl
   conv at A in (fderiv ℝ F _) _ => rw [this]
-  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv 1 (-Complex.I • F) z := by rfl
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ 1 (-Complex.I • F) z := by rfl
   conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
   conv at A =>
     left