From 0a68e3a344cf6b78c0dcb046052b707939327489 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 19 Jun 2024 08:37:14 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 103 +++++++++++++++++++++++++-
 1 file changed, 100 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 591d91f..c537d70 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -4,7 +4,104 @@ import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 
-import Nevanlinna.cauchyRiemann
+
+noncomputable def partialDeriv
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) :=
+  fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))
+
+
+theorem partialDeriv_compContLinAt 
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
+  {f : E → F} 
+  {l : F →L[ℝ] G} 
+  {v : E} 
+  {x : E} 
+  (h : DifferentiableAt ℝ f x) :
+  (partialDeriv v (l ∘ f)) x = (l ∘ partialDeriv v f) x:= by
+  unfold partialDeriv
+  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
+  simp
+
+theorem partialDeriv_compCLE
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
+  {f : E → F}
+  {l : F ≃L[ℝ] G} {v : E} : partialDeriv v (l ∘ f) = l ∘ partialDeriv v f := by
+  funext x
+  by_cases hyp : DifferentiableAt ℝ f x
+  · let lCLM : F →L[ℝ] G := l
+    suffices shyp : partialDeriv v (lCLM ∘ f) x = (lCLM ∘ partialDeriv v f) x from by tauto
+    apply partialDeriv_compContLinAt
+    exact hyp
+  · unfold partialDeriv
+    rw [fderiv_zero_of_not_differentiableAt]
+    simp
+    rw [fderiv_zero_of_not_differentiableAt]
+    simp
+    exact hyp
+    rw [ContinuousLinearEquiv.comp_differentiableAt_iff]
+    exact hyp
+
+theorem partialDeriv_smul'₂
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
+  {f : E → F} {a : ℂ} {v : E} :
+  partialDeriv v (a • f) = a • partialDeriv v f := by
+
+  funext w
+  by_cases ha : a = 0
+  · unfold partialDeriv
+    have : a • f = fun y ↦ a • f y := by rfl
+    rw [this, ha]
+    simp
+  · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence.
+    let smulCLM : F ≃L[ℝ] F :=
+    {
+      toFun := fun x ↦ a • x
+      map_add' := fun x y => DistribSMul.smul_add a x y
+      map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) a x).symm
+      invFun := fun x ↦ a⁻¹ • x
+      left_inv := by
+        intro x
+        simp
+        rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul]
+      right_inv := by
+        intro x
+        simp
+        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul]
+      continuous_toFun := continuous_const_smul a
+      continuous_invFun := continuous_const_smul a⁻¹
+    }
+
+    have : a • f = smulCLM ∘ f := by tauto
+    rw [this]
+    rw [partialDeriv_compCLE]
+    tauto
+
+theorem CauchyRiemann₄
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
+  {f : ℂ → F} : 
+  (Differentiable ℂ f) → partialDeriv Complex.I f = Complex.I • partialDeriv 1 f := by
+  intro h
+  unfold partialDeriv
+
+  conv =>
+    left
+    intro w
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
+    simp
+    rw [← mul_one Complex.I]
+    rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
+  conv =>
+    right
+    right
+    intro w
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
 
 
 theorem MeasureTheory.integral2_divergence₃
@@ -106,9 +203,9 @@ theorem integral_divergence₅
     exact h₁f
 
   let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
-  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ _ F z := by rfl
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv _ F z := by rfl
   conv at A in (fderiv ℝ F _) _ => rw [this]
-  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ _ (-Complex.I • F) z := by rfl
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv _ (-Complex.I • F) z := by rfl
   conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
   conv at A =>
     left