From 6a12258093f067e486abcb53e378629d5a2ae946 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 8 Aug 2024 13:30:59 +0200
Subject: [PATCH] Update holomorphic_examples.lean

---
 Nevanlinna/holomorphic_examples.lean | 56 ++++++++++++++++++----------
 1 file changed, 37 insertions(+), 19 deletions(-)

diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index 5ed5fca..c78a2c2 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -112,7 +112,7 @@ theorem harmonic_is_realOfHolomorphic
   {R : ℝ}
   (hR : 0 < R)
   (hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) :
-  ∃ F : ℂ → ℂ, (∀ z ∈ Metric.ball z R, HolomorphicAt F z) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by
+  ∃ F : ℂ → ℂ, (∀ x ∈ Metric.ball z R, HolomorphicAt F x) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by
 
   let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
   let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
@@ -251,7 +251,7 @@ theorem harmonic_is_realOfHolomorphic
   use F
 
   constructor
-  · -- ∀ (z : ℂ), HolomorphicAt F z
+  · -- ∀ x ∈ Metric.ball z R, HolomorphicAt F x
     intro x hx
     apply HolomorphicAt_iff.2
     use Metric.ball z R
@@ -262,20 +262,21 @@ theorem harmonic_is_realOfHolomorphic
       · intro w hw
         apply (regF w hw).differentiableAt
         apply IsOpen.mem_nhds Metric.isOpen_ball hw
-  · -- (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
+  · -- Set.EqOn (⇑Complex.reCLM ∘ F) f (Metric.ball z R)
+    have : DifferentiableOn ℝ (Complex.reCLM ∘ F) (Metric.ball z R) := by
+      apply DifferentiableOn.comp
+      apply Differentiable.differentiableOn
+      apply ContinuousLinearMap.differentiable Complex.reCLM
+      apply regF.restrictScalars ℝ
+      exact Set.mapsTo'.mpr fun ⦃a⦄ _ => hR
+    have hz : z ∈ Metric.ball z R := by exact Metric.mem_ball_self hR
+    apply Convex.eqOn_of_fderivWithin_eq _ this _ _ _ hz _
+    exact convex_ball z R
+    apply reg₂f.differentiableOn one_le_two
+    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
 
-    apply eq_of_fderiv_eq B A _ 0 C
-
-    intro x
+    intro x hx
+    rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
     rw [fderiv.comp]
     simp
     apply ContinuousLinearMap.ext
@@ -290,7 +291,24 @@ theorem harmonic_is_realOfHolomorphic
     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
+
+    assumption
+    exact ContinuousLinearMap.differentiableAt Complex.reCLM
+    apply (regF.restrictScalars ℝ  x hx).differentiableAt
+    apply IsOpen.mem_nhds Metric.isOpen_ball hx
+    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
+    assumption
+    apply (reg₂f.differentiableOn one_le_two).differentiableAt
+    apply IsOpen.mem_nhds Metric.isOpen_ball hx
+    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
+    assumption
+    -- DifferentiableAt ℝ (⇑Complex.reCLM ∘ F) x
+    apply DifferentiableAt.comp
+    apply Differentiable.differentiableAt
+    exact ContinuousLinearMap.differentiable Complex.reCLM
+    apply (regF.restrictScalars ℝ  x hx).differentiableAt
+    apply IsOpen.mem_nhds Metric.isOpen_ball hx
+    --
+    dsimp [F]
+    rw [primitive_zeroAtBasepoint]
+    simp