English
If Summable u and each f_n is differentiable with a bound on the derivatives, then the tsum of the f_n is differentiable and its derivative is the tsum of the derivatives.
Русский
Если суммируемо u и каждая f_n дифференцируема с ограничением на производные, то сумма по tsum дифференцируема, и её производная равна tsum производных.
LaTeX
$$$$ \text{Differentiable}(\lambda y, \sum_n f_n(y)) \quad\Rightarrow\quad \text{fderiv tsum} = \sum_n \text{fderiv}(f_n). $$$$
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 hasFDerivAt_tsum (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) : HasFDerivAt (fun y => ∑' n, f n y) (∑' n, f' n x) x :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
let A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
exact
hasFDerivAt_tsum_of_isPreconnected hu isOpen_univ isPreconnected_univ (fun n x _ => hf n x) (fun n x _ => hf' n x)
(mem_univ _) hf0 (mem_univ _)
