working…

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
+    apply primitive_differentiable reg₁
-    let A : HasDerivAt (primitive 0 g) (g x) x := primitive_fderiv g reg₁
-    exact A.differentiableAt 
     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
+    fun_prop
-    -- DifferentiableAt ℝ F x
+    -- DifferentiableAt ℝ F x    
     exact regF.restrictScalars ℝ x
+

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}
-  (f : ℂ  → E)
+  (hf : Continuous f)   
-  (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}
-  (f : ℂ  → E)
+  (hf : Differentiable ℂ f)
-  (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
+