English
If Summable u and each g_n is differentiable with bound on g'_n(y), then the tsum of g_n at y0 equals the tsum of derivatives: HasDerivAt (lambda z: tsum g_n(z)) (tsum g'_n(y)) y.
Русский
Если ∑ u сходится и каждый g_n дифференцируем с ограничением на производные, то сумма производных по tsum равна tsum производных.
LaTeX
$$$$\text{HasDerivAt}(\lambda z, \sum_n g_n(z), y) = \sum_n g'_n(y).$$$$
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 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 _)
