Update partialDeriv.lean

Nevanlinna/partialDeriv.lean

@@ -16,6 +16,14 @@ noncomputable def partialDeriv : E → (E → F) → (E → F) :=
   fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v))
 
 
+theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ =ᶠ[nhds x] partialDeriv 𝕜 v f₂ := by
+  unfold partialDeriv
+  intro v
+  apply Filter.EventuallyEq.comp₂
+  exact Filter.EventuallyEq.fderiv h
+  simp
+
+
 theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
   unfold partialDeriv
   conv =>
@@ -85,22 +93,34 @@ theorem partialDeriv_add₂_differentiableAt
   rfl
 
 
-theorem partialDeriv_add₂_differentiableAt'
+theorem partialDeriv_add₂_contDiffAt
   {f₁ f₂ : E → F}
   {v : E}
   {x : E}
-  (h₁ : DifferentiableAt 𝕜 f₁ x)
+  (h₁ : ContDiffAt 𝕜 1 f₁ x)
-  (h₂ : DifferentiableAt 𝕜 f₂ x) :
+  (h₂ : ContDiffAt 𝕜 1 f₂ x) :
   partialDeriv 𝕜 v (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
 
-  unfold partialDeriv
+  obtain ⟨f₁', u₁, hu₁, _, hf₁'⟩ := contDiffAt_one_iff.1 h₁
-  have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
+  obtain ⟨f₂', u₂, hu₂, _, hf₂'⟩ := contDiffAt_one_iff.1 h₂
-  rw [this]
-  rw [fderiv_add h₁ h₂]
-  rfl
 
+  apply Filter.eventuallyEq_iff_exists_mem.2
+  use u₁ ∩ u₂
+  constructor
+  · exact Filter.inter_mem hu₁ hu₂
+  · intro x hx
+    simp
+    apply partialDeriv_add₂_differentiableAt 𝕜 
+    exact (hf₁' x (Set.mem_of_mem_inter_left hx)).differentiableAt
+    exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
+  
 
-theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
+theorem partialDeriv_compContLin 
+  {f : E → F} 
+  {l : F →L[𝕜] G} 
+  {v : E} 
+  (h : Differentiable 𝕜 f) : 
+  partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
   unfold partialDeriv
 
   conv =>
@@ -208,15 +228,6 @@ theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[n
   exact fun v => rfl
 
 
-theorem partialDeriv_eventuallyEq' {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ =ᶠ[nhds x] partialDeriv 𝕜 v f₂ := by
-  unfold partialDeriv
-  intro v
-  let A : fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f₂ := Filter.EventuallyEq.fderiv h
-  apply Filter.EventuallyEq.comp₂
-  exact A
-  simp
-
-
 section restrictScalars
 
 theorem partialDeriv_smul'₂