Saving, renaming

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

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