feat(Analysis/Calculus/Series): specialize to deriv (#9295)

Asked by @MichaelStollBayreuth on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Derivative.20of.20series/near/410063277)

Mathlib/Analysis/Calculus/Series.lean

@@ -98,14 +98,15 @@ theorem continuous_tsum [TopologicalSpace β] {f : α → β → F} (hf : ∀ i,
 
 variable [NormedSpace 𝕜 F]
 
-variable {f : α → E → F} {f' : α → E → E →L[𝕜] F} {v : ℕ → α → ℝ} {s : Set E} {x₀ x : E} {N : ℕ∞}
+variable {f : α → E → F} {f' : α → E → E →L[𝕜] F} {g : α → 𝕜 → F} {g' : α → 𝕜 → F} {v : ℕ → α → ℝ}
+  {s : Set E} {t : Set 𝕜} {x₀ x : E} {y₀ y : 𝕜} {N : ℕ∞}
 
 /-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
 at a point, and all functions in the series are differentiable with a summable bound on the
 derivatives, then the series converges everywhere on the set. -/
 theorem summable_of_summable_hasFDerivAt_of_isPreconnected (hu : Summable u) (hs : IsOpen s)
     (h's : IsPreconnected s) (hf : ∀ n x, x ∈ s → HasFDerivAt (f n) (f' n x) x)
-    (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable (f · x₀)) {x : E}
+    (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s) (hf0 : Summable (f · x₀))
     (hx : x ∈ s) : Summable fun n => f n x := by
   haveI := Classical.decEq α
   rw [summable_iff_cauchySeq_finset] at hf0 ⊢
@@ -117,6 +118,17 @@ theorem summable_of_summable_hasFDerivAt_of_isPreconnected (hu : Summable u) (hs
   exact HasFDerivAt.sum fun i _ => hf i y hy
 #align summable_of_summable_has_fderiv_at_of_is_preconnected summable_of_summable_hasFDerivAt_of_isPreconnected
 
+/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
+at a point, and all functions in the series are differentiable with a summable bound on the
+derivatives, then the series converges everywhere on the set. -/
+theorem summable_of_summable_hasDerivAt_of_isPreconnected (hu : Summable u) (ht : IsOpen t)
+    (h't : IsPreconnected t) (hg : ∀ n y, y ∈ t → HasDerivAt (g n) (g' n y) y)
+    (hg' : ∀ n y, y ∈ t → ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable (g · y₀))
+    (hy : y ∈ t) : Summable fun n => g n y := by
+  simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
+  refine summable_of_summable_hasFDerivAt_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
+  simpa? says simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]
+
 /-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
 at a point, and all functions in the series are differentiable with a summable bound on the
 derivatives, then the series is differentiable on the set and its derivative is the sum of the
@@ -136,6 +148,20 @@ theorem hasFDerivAt_tsum_of_isPreconnected (hu : Summable u) (hs : IsOpen s)
     exact HasFDerivAt.sum fun n _ => hf n y hy
 #align has_fderiv_at_tsum_of_is_preconnected hasFDerivAt_tsum_of_isPreconnected
 
+/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
+at a point, and all functions in the series are differentiable with a summable bound on the
+derivatives, then the series is differentiable on the set and its derivative is the sum of the
+derivatives. -/
+theorem hasDerivAt_tsum_of_isPreconnected (hu : Summable u) (ht : IsOpen t)
+    (h't : IsPreconnected t) (hg : ∀ n y, y ∈ t → HasDerivAt (g n) (g' n y) y)
+    (hg' : ∀ n y, y ∈ t → ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t) (hg0 : Summable fun n => g n y₀)
+    (hy : y ∈ t) : HasDerivAt (fun z => ∑' n, g n z) (∑' n, g' n y) y := by
+  simp_rw [hasDerivAt_iff_hasFDerivAt] at hg ⊢
+  convert hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
+  · exact (ContinuousLinearMap.smulRightL 𝕜 𝕜 F 1).map_tsum <|
+      .of_norm_bounded u hu fun n ↦ hg' n y hy
+  · simpa? says simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]
+
 /-- Consider a series of functions `∑' n, f n x`. If the series converges at a
 point, and all functions in the series are differentiable with a summable bound on the derivatives,
 then the series converges everywhere. -/
@@ -147,6 +173,15 @@ theorem summable_of_summable_hasFDerivAt (hu : Summable u)
     (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)
 #align summable_of_summable_has_fderiv_at summable_of_summable_hasFDerivAt
 
+/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
+point, and all functions in the series are differentiable with a summable bound on the derivatives,
+then the series converges everywhere. -/
+theorem summable_of_summable_hasDerivAt (hu : Summable u)
+    (hg : ∀ n y, HasDerivAt (g n) (g' n y) y) (hg' : ∀ n y, ‖g' n y‖ ≤ u n)
+    (hg0 : Summable fun n => g n y₀) (y : 𝕜) : Summable fun n => g n y := by
+  exact summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
+    (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (mem_univ _)
+
 /-- Consider a series of functions `∑' n, f n x`. If the series converges at a
 point, and all functions in the series are differentiable with a summable bound on the derivatives,
 then the series is differentiable and its derivative is the sum of the derivatives. -/
@@ -158,6 +193,15 @@ theorem hasFDerivAt_tsum (hu : Summable u) (hf : ∀ n x, HasFDerivAt (f n) (f'
     (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)
 #align has_fderiv_at_tsum hasFDerivAt_tsum
 
+/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
+point, and all functions in the series are differentiable with a summable bound on the derivatives,
+then the series is differentiable and its derivative is the sum of the derivatives. -/
+theorem hasDerivAt_tsum (hu : Summable u) (hg : ∀ n y, HasDerivAt (g n) (g' n y) y)
+    (hg' : ∀ n y, ‖g' n y‖ ≤ u n) (hg0 : Summable fun n => g n y₀) (y : 𝕜) :
+    HasDerivAt (fun z => ∑' n, g n z) (∑' n, g' n y) y := by
+  exact hasDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ
+    (fun n y _ => hg n y) (fun n y _ => hg' n y) (mem_univ _) hg0 (mem_univ _)
+
 /-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
 with a summable bound on the derivatives, then the series is differentiable.
 Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
@@ -174,19 +218,40 @@ theorem differentiable_tsum (hu : Summable u) (hf : ∀ n x, HasFDerivAt (f n) (
     exact differentiable_const 0
 #align differentiable_tsum differentiable_tsum
 
+/-- Consider a series of functions `∑' n, f n x`. If all functions in the series are differentiable
+with a summable bound on the derivatives, then the series is differentiable.
+Note that our assumptions do not ensure the pointwise convergence, but if there is no pointwise
+convergence then the series is zero everywhere so the result still holds. -/
+theorem differentiable_tsum' (hu : Summable u) (hg : ∀ n y, HasDerivAt (g n) (g' n y) y)
+    (hg' : ∀ n y, ‖g' n y‖ ≤ u n) : Differentiable 𝕜 fun z => ∑' n, g n z := by
+  simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
+  refine differentiable_tsum hu hg ?_
+  simpa? says simpa only [ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]
+
 theorem fderiv_tsum_apply (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n))
     (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) (x : E) :
     fderiv 𝕜 (fun y => ∑' n, f n y) x = ∑' n, fderiv 𝕜 (f n) x :=
   (hasFDerivAt_tsum hu (fun n x => (hf n x).hasFDerivAt) hf' hf0 _).fderiv
 #align fderiv_tsum_apply fderiv_tsum_apply
 
+theorem deriv_tsum_apply (hu : Summable u) (hg : ∀ n, Differentiable 𝕜 (g n))
+    (hg' : ∀ n y, ‖deriv (g n) y‖ ≤ u n) (hg0 : Summable fun n => g n y₀) (y : 𝕜) :
+    deriv (fun z => ∑' n, g n z) y = ∑' n, deriv (g n) y :=
+  (hasDerivAt_tsum hu (fun n y => (hg n y).hasDerivAt) hg' hg0 _).deriv
+
 theorem fderiv_tsum (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n))
-    (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) {x₀ : E} (hf0 : Summable fun n => f n x₀) :
+    (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) :
     (fderiv 𝕜 fun y => ∑' n, f n y) = fun x => ∑' n, fderiv 𝕜 (f n) x := by
   ext1 x
   exact fderiv_tsum_apply hu hf hf' hf0 x
 #align fderiv_tsum fderiv_tsum
 
+theorem deriv_tsum (hu : Summable u) (hg : ∀ n, Differentiable 𝕜 (g n))
+    (hg' : ∀ n y, ‖deriv (g n) y‖ ≤ u n) (hg0 : Summable fun n => g n y₀) :
+    (deriv fun y => ∑' n, g n y) = fun y => ∑' n, deriv (g n) y := by
+  ext1 x
+  exact deriv_tsum_apply hu hg hg' hg0 x
+
 /-! ### Higher smoothness -/
 
 /-- Consider a series of smooth functions, with summable uniform bounds on the successive