working…

Nevanlinna/holomorphic_examples.lean

@@ -1,4 +1,3 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
 import Nevanlinna.holomorphic_primitive
@@ -107,7 +106,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 ∧ ((F z).re = f z)) := by
+  ∃ F : ℂ → ℂ, ∀ z, HolomorphicAt F z ∧ (Complex.reCLM ∘ F = f) := by
 
   let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
   let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
@@ -194,20 +193,64 @@ 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
+    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₁
+
   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
-    
-    sorry
+    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
+

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