English
If Summable u and each f_n is differentiable with HasFDerivAt with derivative f'_n(x), and Summable derivatives norm-wise, then the derivative of the tsum equals tsum of derivatives: fderiv 𝕜 (λ y, ∑' n f_n(y)) x = ∑' n f'_n(x).
Русский
Если сумма ∑ u(n) сходится и f_n дифференцируемы с производной f'_n, и нормы производных суммируемы, то производная суммы равна сумме производных.
LaTeX
$$$$ \operatorname{fderiv}_𝕜\bigl(\lambda y, \sum_n f_n(y)\bigr)(x) = \sum_n f'_n(x). $$$$
Lean4
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
