English
If every f_n is differentiable with a uniform derivative bound and there is no point x0 where ∑ f_n(x0) converges, then the sum function is identically zero, hence differentiable. If there exists x0 with convergence, the sum is differentiable there and elsewhere by the previous results.
Русский
Если каждое f_n дифференцируемо и имеет общую предел_bound на производную, и не существует x0, для которого сумма ∑ f_n(x0) сходится, то сумма функций равна нулю, следовательно, дифференцируема. Если существует x0, где сумма сходится, функция суммы дифференцируема на всей области, по предыдущим результатам.
LaTeX
$$$$\exists x_0: E, \ Summable(\lambda n, f_n(x_0)) \Rightarrow \text{Differentiable}(\lambda y, \sum_n f_n(y))$$ and if not, the sum is identically zero.$$
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_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 _)
