From 6061fa4279e98dd82a8fd2e949aa52ae5ef3c149 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 7 May 2024 17:32:41 +0200
Subject: [PATCH] Update partialDeriv.lean

---
 Nevanlinna/partialDeriv.lean | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 20be9da..79d11eb 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -9,13 +9,15 @@ import Mathlib.Analysis.Calculus.FDeriv.Comp
 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 : ℂ → (ℂ → ℂ) → (ℂ → ℂ) :=
+noncomputable def Real.partialDeriv : E → (E → F) → (E → F) :=
   fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))
 
 
-
-theorem partialDeriv_smul₁ {f : ℂ → ℂ} {a : ℝ} {v : ℂ} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
+theorem partialDeriv_smul₁ {f : E → F} {a : ℝ} {v : E} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
   unfold Real.partialDeriv
   conv =>
     left
@@ -23,7 +25,7 @@ theorem partialDeriv_smul₁ {f : ℂ → ℂ} {a : ℝ} {v : ℂ} : Real.partia
     rw [map_smul]
 
 
-theorem partialDeriv_add₁ {f : ℂ → ℂ} {v₁ v₂ : ℂ} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by
+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
   conv =>
     left
@@ -31,7 +33,7 @@ theorem partialDeriv_add₁ {f : ℂ → ℂ} {v₁ v₂ : ℂ} : Real.partialDe
     rw [map_add]
 
 
-theorem partialDeriv_smul₂ {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
+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
 
   have : a • f = fun y ↦ a • f y := by rfl
@@ -43,7 +45,7 @@ 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
+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
 
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
@@ -55,7 +57,7 @@ theorem partialDeriv_add₂ {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differen
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
-theorem partialDeriv_compContLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
+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
 
   conv =>
@@ -67,7 +69,7 @@ theorem partialDeriv_compContLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v :
   rfl
 
 
-theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n + 1) f) : ∀ v : ℂ, ContDiff ℝ n (Real.partialDeriv v f) := by
+theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1) f) : ∀ v : E, ContDiff ℝ n (Real.partialDeriv v f) := by
   unfold Real.partialDeriv
   intro v
 
@@ -85,7 +87,7 @@ theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n +
   exact contDiff_const
 
 
-lemma partialDeriv_fderiv {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
+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
 
   unfold Real.partialDeriv
@@ -95,8 +97,8 @@ lemma partialDeriv_fderiv {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ
   · simp
 
 
-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
+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
 
   intro v₁ v₂
   funext z