Working on partial derivatives

Nevanlinna/complexHarmonic.lean

@@ -6,17 +6,13 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Nevanlinna.cauchyRiemann
-
-noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) := by
-  intro v
-  intro f
-  exact fun w ↦ (fderiv ℝ f w) v
+import Nevanlinna.partialDeriv
 
 theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
   → Real.partialDeriv Complex.I f = Complex.I • Real.partialDeriv 1 f := by
   intro h
   unfold Real.partialDeriv
-  
+
   conv =>
     left
     intro w
@@ -28,26 +24,15 @@ theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
   conv =>
     right
     right
-    intro w    
+    intro w
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
 
-theorem partialDeriv_smul {f : ℂ → ℂ } {a v : ℂ } : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
-  unfold Real.partialDeriv
-  have : a • f = fun y ↦ a • f y := by rfl
-  conv =>
-    left
-    intro w
-    rw [this]
-    rw [fderiv_const_smul]
-    
-  
-  sorry
 
 noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
   intro f
   let fx  := Real.partialDeriv 1 f
   let fxx := Real.partialDeriv 1 fx
-  let fy  := Real.partialDeriv Complex.I f 
+  let fy  := Real.partialDeriv Complex.I f
   let fyy := Real.partialDeriv Complex.I fy
   exact fxx + fyy
 
@@ -86,6 +71,7 @@ lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
   · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
   · simp
 
+#check partialDeriv_contDiff
 
 theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   Harmonic f := by
@@ -94,6 +80,14 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   have f_is_real_C2 : ContDiff ℝ 2 f :=
     ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
+  -- f is real differentiable
+  have f_is_real_differentiable : Differentiable ℝ f := by
+    exact (contDiff_succ_iff_fderiv.1 f_is_real_C2).left
+
+  have fI_is_real_differentiable : Differentiable ℝ (Real.partialDeriv 1 f) := by
+    let A := partialDeriv_contDiff f_is_real_C2 1
+    exact (contDiff_succ_iff_fderiv.1 A).left
+
   -- f' is real C¹
   have f'_is_real_C1 : ContDiff ℝ 1 (fderiv ℝ f) :=
     (contDiff_succ_iff_fderiv.1 f_is_real_C2).right
@@ -117,16 +111,9 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
     unfold Complex.laplace
 
     rw [CauchyRiemann₄ h]
+    rw [partialDeriv_smul fI_is_real_differentiable]
 
 
-
-    have t₁a : (fderiv ℝ (fun w ↦ Complex.I * (fderiv ℝ f w) 1) z) 
-      = Complex.I • (fderiv ℝ f_1 z) := by
-      rw [fderiv_const_mul]
-      fun_prop
-
-    rw [t₁a]
-
     have t₂ : (fderiv ℝ f_1 z) Complex.I = (fderiv ℝ f_I z) 1 := by
       let B := l₂ f_is_real_C2 z Complex.I 1
       rw [← B]
@@ -146,7 +133,7 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
       intro z
       simp [f_I]
       rw [CauchyRiemann₁ (h z)]
-    
+
     rw [t₁a]
 
     simp

Nevanlinna/partialDeriv.lean

@@ -0,0 +1,44 @@
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Defs
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+
+
+noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) := by
+  intro v
+  intro f
+  exact fun w ↦ (fderiv ℝ f w) v
+
+
+theorem partialDeriv_smul {f : ℂ → ℂ } {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
+  unfold Real.partialDeriv
+
+  have : a • f = fun y ↦ a • f y := by rfl
+  rw [this]
+
+  conv =>
+    left
+    intro w
+    rw [fderiv_const_smul (h w)]
+
+
+theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n + 1) f) : ∀ v : ℂ, ContDiff ℝ n (Real.partialDeriv v f) := by
+  unfold Real.partialDeriv
+  intro v
+
+  let A := (contDiff_succ_iff_fderiv.1 h).right
+  simp at A
+
+  have : (fun w => (fderiv ℝ f w) v) = (fun f => f v) ∘ (fun w => (fderiv ℝ f w)) := by
+    rfl
+
+  rw [this]
+  refine ContDiff.comp ?hg A
+  refine ContDiff.of_succ ?hg.h
+  refine ContDiff.clm_apply ?hg.h.hf ?hg.h.hg
+  exact contDiff_id
+  exact contDiff_const