Nevanlinna/holomorphic_examples.lean

@@ -1,3 +1,4 @@
+import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
 import Nevanlinna.holomorphic_primitive
@@ -106,7 +107,7 @@ A harmonic, real-valued function on ℂ is the real part of a suitable holomorph
 theorem harmonic_is_realOfHolomorphic
   {f : ℂ → ℝ}
   (hf : ∀ z, HarmonicAt f z) :
-  ∃ F : ℂ → ℂ, ∀ z, HolomorphicAt F z ∧ (Complex.reCLM ∘ F = f) := by
+  ∃ F : ℂ → ℂ, ∀ z, (HolomorphicAt F z ∧ ((F z).re = f z)) := by
 
   let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
   let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
@@ -193,64 +194,20 @@ theorem harmonic_is_realOfHolomorphic
       apply Differentiable.const_smul
       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
-    apply primitive_differentiable reg₁
-    simp
-
-  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by 
-    intro x
-    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x)]
-    dsimp [F]
-    rw [fderiv_add_const]
-    rw [primitive_fderiv']
-    exact rfl
-    exact reg₁
-
+  let F := primitive 0 g
   use F
   intro z
   constructor
   · -- HolomorphicAt F z
     apply HolomorphicAt_iff.2
-    use Set.univ
+    use {z : ℂ | true}
     constructor
     · exact isOpen_const
     · constructor
       · simp
-      · intro w _
-        exact regF w
+      · intro w hw
+        let A : HasDerivAt (primitive 0 g) (g w) w := primitive_fderiv g reg₁
+        apply A.differentiableAt
   · -- (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 
-      dsimp [F]
-      rw [primitive_zeroAtBasepoint]
-      simp
-
-    apply eq_of_fderiv_eq B A _ 0 C
-
-    intro x
-    rw [fderiv.comp]
-    simp
-    apply ContinuousLinearMap.ext
-    intro w
-    simp
-    rw [pF'']
-    dsimp [g, f_1, f_I, partialDeriv]
-    simp
-    have : w = w.re • 1 + w.im • Complex.I := by simp
-    nth_rw 3 [this]
-    rw [(fderiv ℝ f x).map_add]
-    rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
-    rw [smul_eq_mul, smul_eq_mul]
-    ring
-    -- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
-    fun_prop
-    -- DifferentiableAt ℝ F x    
-    exact regF.restrictScalars ℝ x
-
+    
+    sorry

Nevanlinna/holomorphic_primitive.lean

@@ -485,11 +485,11 @@ theorem primitive_translation
   simp
 
 
-theorem primitive_hasDerivAtBasepoint
+theorem primitive_fderivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Continuous f)   
-  (z₀ : ℂ) :
+  {z₀ : ℂ}
+  (f : ℂ  → E)
+  (hf : Continuous f) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
@@ -597,70 +597,15 @@ theorem primitive_additivity
   abel
 
 
-theorem primitive_hasDerivAt
+theorem primitive_fderiv
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ z : ℂ) :
+  {z₀ z : ℂ}
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f) :
   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_hasDerivAtBasepoint
+  apply primitive_fderivAtBasepoint
   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
-