English
If a family f_i is ContDiff of order N and there are uniform summable bounds on all iterated derivatives up to order N, then the sum ∑' f_i is ContDiff of order N and iterated derivatives distribute over tsum.
Русский
Если семейство f_i имеет класс C^N и существуют единообразные суммируемые пределы на все производные 1–й, …, N-й степеней, то сумма ∑' f_i тоже C^N, и итеративные производные суммирования равны суммам соответствующих производных.
LaTeX
$$$$ \text{contDiff}_𝕜\; N\; (\lambda x, \sum_i f_i(x)) $$ and $$ \text{iteratedFDeriv}_𝕜 k(\lambda x, \sum_i f_i(x)) = \sum_i \text{iteratedFDeriv}_𝕜 k( f_i )(x). $$$$
Lean4
theorem deriv_tsum_apply (hu : Summable u) (hg : ∀ n, Differentiable 𝕜 (g n)) (hg' : ∀ n y, ‖deriv (g n) y‖ ≤ u n)
(hg0 : Summable fun n => g n y₀) (y : 𝕜) : deriv (fun z => ∑' n, g n z) y = ∑' n, deriv (g n) y :=
(hasDerivAt_tsum hu (fun n y => (hg n y).hasDerivAt) hg' hg0 _).deriv
