From 1d27eeb66b97951d4d78640047fe087bf51919b3 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 14:11:39 +0200
Subject: [PATCH] Working.

---
 Nevanlinna/holomorphic_examples.lean | 36 +++++++++++++++++++++++++---
 1 file changed, 33 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index f4062d2..cdf69a5 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/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