Define partial over arbitrary fields

Nevanlinna/cauchyRiemann.lean

@@ -45,9 +45,9 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
 
 
 theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
-  → Real.partialDeriv Complex.I f = Complex.I • Real.partialDeriv 1 f := by
+  → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
-  unfold Real.partialDeriv
+  unfold partialDeriv
 
   conv =>
     left

Nevanlinna/complexHarmonic.lean

@@ -17,10 +17,10 @@ import Nevanlinna.partialDeriv
 
 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 fyy := Real.partialDeriv Complex.I fy
+  let fx  := partialDeriv ℝ 1 f
+  let fxx := partialDeriv ℝ 1 fx
+  let fy  := partialDeriv ℝ Complex.I f
+  let fyy := partialDeriv ℝ Complex.I fy
   exact fxx + fyy
 
 
@@ -35,8 +35,8 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   have f_is_real_C2 : ContDiff ℝ 2 f :=
     ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-  have fI_is_real_differentiable : Differentiable ℝ (Real.partialDeriv 1 f) := by
-    exact (partialDeriv_contDiff f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
+  have fI_is_real_differentiable : Differentiable ℝ (partialDeriv ℝ 1 f) := by
+    exact (partialDeriv_contDiff ℝ f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)
 
   constructor
   · -- f is two times real continuously differentiable
@@ -49,7 +49,7 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
     -- This lemma says that partial derivatives commute with complex scalar
     -- multiplication. This is a consequence of partialDeriv_compContLin once we
     -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g →  Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by
+    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
       intro v s g hg
 
       -- Present scalar multiplication as a continuous ℝ-linear map. This is
@@ -71,7 +71,7 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
       have : s • g = sMuls ∘ g := by rfl
       rw [this]
 
-      rw [partialDeriv_compContLin hg]
+      rw [partialDeriv_compContLin ℝ hg]
       rfl
 
     rw [this]

Nevanlinna/partialDeriv.lean

@@ -10,31 +10,33 @@ import Mathlib.Analysis.Calculus.FDeriv.Linear
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-
-noncomputable def Real.partialDeriv : E → (E → F) → (E → F) :=
-  fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable (𝕜)
 
 
-theorem partialDeriv_smul₁ {f : E → F} {a : ℝ} {v : E} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
-  unfold Real.partialDeriv
+noncomputable def partialDeriv : E → (E → F) → (E → F) :=
+  fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v))
+
+
+theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
+  unfold partialDeriv
   conv =>
     left
     intro w
     rw [map_smul]
 
 
-theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by
-  unfold Real.partialDeriv
+theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by
+  unfold partialDeriv
   conv =>
     left
     intro w
     rw [map_add]
 
 
-theorem partialDeriv_smul₂ {f : E → F} {a : ℝ} {v : E} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
-  unfold Real.partialDeriv
+theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
+  unfold partialDeriv
 
   have : a • f = fun y ↦ a • f y := by rfl
   rw [this]
@@ -45,8 +47,8 @@ theorem partialDeriv_smul₂ {f : E → F} {a : ℝ} {v : E} (h : Differentiable
     rw [fderiv_const_smul (h w)]
 
 
-theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable ℝ f₁)  (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
-  unfold Real.partialDeriv
+theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁)  (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
+  unfold partialDeriv
 
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
   rw [this]
@@ -57,8 +59,8 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
-theorem partialDeriv_compContLin {f : E → F} {l : F →L[ℝ] F} {v : E} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
-  unfold Real.partialDeriv
+theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] F} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
+  unfold partialDeriv
 
   conv =>
     left
@@ -69,14 +71,14 @@ theorem partialDeriv_compContLin {f : E → F} {l : F →L[ℝ] F} {v : E} (h :
   rfl
 
 
-theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1) f) : ∀ v : E, ContDiff ℝ n (Real.partialDeriv v f) := by
-  unfold Real.partialDeriv
+theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by
+  unfold 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
+  have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
     rfl
 
   rw [this]
@@ -87,18 +89,21 @@ theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1)
   exact contDiff_const
 
 
-lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff ℝ 2 f) (z a b : E) :
-    fderiv ℝ (fderiv ℝ f) z b a = Real.partialDeriv b (Real.partialDeriv a f) z := by
+lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :
+    fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by
 
-  unfold Real.partialDeriv
+  unfold partialDeriv
   rw [fderiv_clm_apply]
   · simp
   · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
   · simp
 
 
-theorem partialDeriv_comm {f : E → F} (h : ContDiff ℝ 2 f) :
-  ∀ v₁ v₂ : E, Real.partialDeriv v₁ (Real.partialDeriv v₂ f) = Real.partialDeriv v₂ (Real.partialDeriv v₁ f) := by
+theorem partialDeriv_comm
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {f : E → F} (h : ContDiff ℝ 2 f) :
+  ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) := by
 
   intro v₁ v₂
   funext z
@@ -118,7 +123,6 @@ theorem partialDeriv_comm {f : E → F} (h : ContDiff ℝ 2 f) :
 
     apply second_derivative_symmetric h₀ h₁ v₁ v₂
 
-
-  rw [← partialDeriv_fderiv h z v₂ v₁]
+  rw [← partialDeriv_fderiv ℝ h z v₂ v₁]
   rw [derivSymm]
-  rw [partialDeriv_fderiv h z v₁ v₂]
+  rw [partialDeriv_fderiv ℝ h z v₁ v₂]