English
Under hypotheses of iterated derivatives with uniform summable bounds, the tsum of iterated derivatives equals the iterated derivative of sum: iteratedFDeriv k (λ y, ∑' n f_n y) x = ∑' n iteratedFDeriv k (f_n) x.
Русский
При условиях на итеративные производные с равномерными суммируемыми границами, сумма итеративных производных равна итеративной производной суммы: iteratedFDeriv k(λ y, ∑' n f_n y) x = ∑' n iteratedFDeriv k (f_n) x.
LaTeX
$$$$ \text{iteratedFDeriv}_𝕜 k(\lambda y, \sum_n f_n(y)) = \sum_n \text{iteratedFDeriv}_𝕜 k(f_n). $$$$
Lean4
theorem fderiv_tsum (hu : Summable u) (hf : ∀ n, Differentiable 𝕜 (f n)) (hf' : ∀ n x, ‖fderiv 𝕜 (f n) x‖ ≤ u n)
(hf0 : Summable fun n => f n x₀) : (fderiv 𝕜 fun y => ∑' n, f n y) = fun x => ∑' n, fderiv 𝕜 (f n) x :=
by
ext1 x
exact fderiv_tsum_apply hu hf hf' hf0 x
