English
If the series is not pointwise convergent everywhere, the sum is identically zero; otherwise, under summability and differentiability conditions, the sum is differentiable.
Русский
Если ряд не сходится по точкам повсеместно, сумма нулевая; иначе, при условии суммируемости и дифференцируемости сумма дифференцируема.
LaTeX
$$$$ \text{if not convergent } \sum_n f_n(x)=0; \text{ else, differentiable.} $$$$
Lean4
/-- Consider a series of smooth functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative. -/
theorem iteratedFDeriv_tsum_apply (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, (k : ℕ∞) ≤ N → Summable (v k))
(h'f : ∀ (k : ℕ) (i : α) (x : E), (k : ℕ∞) ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) {k : ℕ} (hk : (k : ℕ∞) ≤ N)
(x : E) : iteratedFDeriv 𝕜 k (fun y => ∑' n, f n y) x = ∑' n, iteratedFDeriv 𝕜 k (f n) x := by
rw [iteratedFDeriv_tsum hf hv h'f hk]
