English
If Summable u and f_n with HasFDerivAt(f_n) and bound ||f'_n(x)|| ≤ u_n hold, then the tsum of derivatives equals the derivative tsum: fderiv 𝕜 (λ y. ∑' n f_n(y)) x = ∑' n f'_n(x).
Русский
При условии суммируемости u и наличии f_n с HasFDerivAt и ограничением ||f'_n(x)|| ≤ u_n, производная суммирования равна сумме производных: fderiv x (λ y. ∑' n f_n(y)) = ∑' n f'_n(x).
LaTeX
$$$$\operatorname{fderiv}\bigl(\lambda y. \sum_n f_n(y)\bigr)(x) = \sum_n f'_n(x).$$$$
Lean4
/-- 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_hasFDerivAt (hu : Summable u) (hf : ∀ n x, HasFDerivAt (f n) (f' n x) x)
(hf' : ∀ n x, ‖f' n x‖ ≤ u n) (hf0 : Summable fun n => f n x₀) (x : E) : Summable fun n => f n x :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
exact
summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ (fun n x _ => hf n x)
(fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)
