English
If Summable u and g_n are differentiable with derivatives bounds, then the tsum identity holds for deriv: deriv( λ z, ∑' n, g_n(z) ) = ∑' n deriv(g_n)(z).
Русский
Если сумма u сходится и g_n дифференцируемы с ограничениями на производные, то производная суммы равна сумме производных: deriv(∑ g_n) = ∑ deriv(g_n).
LaTeX
$$$$ \frac{d}{dz}\left(\sum_n g_n(z)\right) = \sum_n \frac{d}{dz} g_n(z). $$$$
Lean4
theorem deriv_tsum (hu : Summable u) (hg : ∀ n, Differentiable 𝕜 (g n)) (hg' : ∀ n y, ‖deriv (g n) y‖ ≤ u n)
(hg0 : Summable fun n => g n y₀) : (deriv fun y => ∑' n, g n y) = fun y => ∑' n, deriv (g n) y :=
by
ext1 x
exact deriv_tsum_apply hu hg hg' hg0 x
