Working.

Nevanlinna/holomorphic_examples.lean

@@ -107,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 ∧ ((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)
@@ -195,6 +195,12 @@ theorem harmonic_is_realOfHolomorphic
       exact reg₁f_I.differentiable le_rfl
   
   let F := primitive 0 g
+
+  have pF : ∀ x a, (fderiv ℝ F x) a = (g x) * a := by 
+    sorry
+
+  have regF : Differentiable ℂ F := by sorry
+
   use F
   intro z
   constructor
@@ -209,5 +215,29 @@ theorem harmonic_is_realOfHolomorphic
         let A : HasDerivAt (primitive 0 g) (g w) w := primitive_fderiv g reg₁
         apply A.differentiableAt
   · -- (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 sorry
+    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)
+    exact ContinuousLinearMap.differentiableAt Complex.reCLM
+    -- DifferentiableAt ℝ F x
+    exact regF.restrictScalars ℝ x