Big cleanup

Nevanlinna/cauchyRiemann.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
 import Mathlib.Analysis.Complex.RealDeriv
+import Nevanlinna.partialDeriv
 
 variable {z : ℂ} {f : ℂ → ℂ}
 
@@ -41,3 +42,23 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
     rw [ContinuousLinearMap.comp_lineDeriv]
   rw [CauchyRiemann₁ h, Complex.I_mul]
   simp
+
+
+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
+    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)]

Nevanlinna/complexHarmonic.lean

@@ -8,25 +8,6 @@ import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Nevanlinna.cauchyRiemann
 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
-    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)]
-
 
 noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
   intro f
@@ -41,37 +22,6 @@ def Harmonic (f : ℂ → ℂ) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
-lemma derivSymm (f : ℂ → ℂ) (hf : ContDiff ℝ 2 f) :
-  ∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
-  intro z a b
-
-  let f' := fderiv ℝ f
-  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
-    have h : Differentiable ℝ f := by
-      exact (contDiff_succ_iff_fderiv.1 hf).left
-    exact fun y => DifferentiableAt.hasFDerivAt (h y)
-
-  let f'' := (fderiv ℝ f' z)
-  have h₁ : HasFDerivAt f' f'' z := by
-    apply DifferentiableAt.hasFDerivAt
-    let A := (contDiff_succ_iff_fderiv.1 hf).right
-    let B := (contDiff_succ_iff_fderiv.1 A).left
-    simp at B
-    exact B z
-
-  let A := second_derivative_symmetric h₀ h₁ a b
-  dsimp [f'', f'] at A
-  apply A
-
-
-lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
-    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
-  rw [fderiv_clm_apply]
-  · simp
-  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
-  · simp
-
-
 theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   Harmonic f := by
 

Nevanlinna/partialDeriv.lean

@@ -5,16 +5,16 @@ 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.Comp
+import Mathlib.Analysis.Calculus.FDeriv.Linear
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 
 
-noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) := by
-  intro v
-  intro f
-  exact fun w ↦ (fderiv ℝ f w) v
+noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) :=
+  fun v ↦ (fun f ↦ (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
+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
@@ -26,6 +26,30 @@ theorem partialDeriv_smul {f : ℂ → ℂ } {a v : ℂ} (h : Differentiable ℝ
     rw [fderiv_const_smul (h w)]
 
 
+theorem partialDeriv_add {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentiable ℝ f₁)  (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
+  unfold Real.partialDeriv
+
+  have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
+  rw [this]
+  conv =>
+    left
+    intro w
+    left
+    rw [fderiv_add (h₁ w) (h₂ w)]
+
+
+theorem partialDeriv_compLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
+  unfold Real.partialDeriv
+
+  conv =>
+    left
+    intro w
+    left
+    rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
+  simp
+  rfl
+
+
 theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n + 1) f) : ∀ v : ℂ, ContDiff ℝ n (Real.partialDeriv v f) := by
   unfold Real.partialDeriv
   intro v
@@ -44,50 +68,38 @@ theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n +
   exact contDiff_const
 
 
-lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
-    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
+lemma partialDeriv_fderiv {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
+    fderiv ℝ (fderiv ℝ f) z b a = Real.partialDeriv b (Real.partialDeriv a f) z := by
+
+  unfold Real.partialDeriv
   rw [fderiv_clm_apply]
   · simp
   · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
   · simp
 
 
-lemma derivSymm (f : ℂ → ℂ) (hf : ContDiff ℝ 2 f) :
-  ∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
-  intro z a b
-
-  let f' := fderiv ℝ f
-  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
-    have h : Differentiable ℝ f := by
-      exact (contDiff_succ_iff_fderiv.1 hf).left
-    exact fun y => DifferentiableAt.hasFDerivAt (h y)
-
-  let f'' := (fderiv ℝ f' z)
-  have h₁ : HasFDerivAt f' f'' z := by
-    apply DifferentiableAt.hasFDerivAt
-    let A := (contDiff_succ_iff_fderiv.1 hf).right
-    let B := (contDiff_succ_iff_fderiv.1 A).left
-    simp at B
-    exact B z
-
-  let A := second_derivative_symmetric h₀ h₁ a b
-  dsimp [f'', f'] at A
-  apply A
-
-
 theorem partialDeriv_comm {f : ℂ → ℂ} (h : ContDiff ℝ 2 f) :
   ∀ v₁ v₂ : ℂ, Real.partialDeriv v₁ (Real.partialDeriv v₂ f) = Real.partialDeriv v₂ (Real.partialDeriv v₁ f) := by
 
   intro v₁ v₂
-  unfold Real.partialDeriv
   funext z
 
-  conv =>
-    left
-    rw [← l₂ h z v₂ v₁]
+  have derivSymm :
+    (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by
 
-  rw [derivSymm f h z v₁ v₂]
+    let f' := fderiv ℝ f
+    have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
+      intro y
+      exact DifferentiableAt.hasFDerivAt ((h.differentiable one_le_two) y)
 
-  conv =>
-    left
-    rw [l₂ h z v₁ v₂]
+    let f'' := (fderiv ℝ f' z)
+    have h₁ : HasFDerivAt f' f'' z := by
+      apply DifferentiableAt.hasFDerivAt
+      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
+
+    apply second_derivative_symmetric h₀ h₁ v₁ v₂
+
+
+  rw [← partialDeriv_fderiv h z v₂ v₁]
+  rw [derivSymm]
+  rw [partialDeriv_fderiv h z v₁ v₂]