English
If Summable u and g_n are differentiable on a preconnected set t with HasDerivAt(g_n, g'_n(y), y) and ||g'_n(y)|| ≤ u_n, the derivative of the sum ∑' g_n is the sum of derivatives: HasDerivAt (y ↦ ∑' n, g_n(y)) (∑' n g'_n(y)) y.
Русский
Если ∑ u(n) сходится и функции g_n дифференцируемы на предсвязанном множестве t с HasDerivAt(g_n, g'_n(y), y) и ||g'_n(y)|| ≤ u_n, то производная суммы ∑' g_n равна сумме производных: HasDerivAt( y ↦ ∑' n g_n(y) ) (∑' n g'_n(y)) y.
LaTeX
$$$$\text{HasDerivAt}\left(\lambda y. \sum_n g_n(y)\right)\left(\sum_n g'_n(y)\right) y,$$$$
Lean4
/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. 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 on the set and its derivative is the sum of the
derivatives. -/
theorem hasDerivAt_tsum_of_isPreconnected (hu : Summable u) (ht : IsOpen t) (h't : IsPreconnected t)
(hg : ∀ n y, y ∈ t → HasDerivAt (g n) (g' n y) y) (hg' : ∀ n y, y ∈ t → ‖g' n y‖ ≤ u n) (hy₀ : y₀ ∈ t)
(hg0 : Summable fun n => g n y₀) (hy : y ∈ t) : HasDerivAt (fun z => ∑' n, g n z) (∑' n, g' n y) y :=
by
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg ⊢
convert hasFDerivAt_tsum_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
· exact (ContinuousLinearMap.smulRightL 𝕜 𝕜 F 1).map_tsum <| .of_norm_bounded hu fun n ↦ hg' n y hy
· simpa
