English
Under the hypotheses that Summable u and HasFDerivAt for each f_n with a uniform derivative bound, the derivative of the sum ∑' f_n is the sum of the derivatives: HasFDerivAt (y ↦ ∑' n, f_n(y)) (∑' n, f'_n(x)) x.
Русский
При условиях, что ∑ u(n) сходится и для каждого f_n верна равенство HasFDerivAt с однородной границей производной, производная суммы фунций равна сумме производных: HasFDerivAt (y ↦ ∑' n f_n(y)) (∑' n f'_n(x)) x.
LaTeX
$$$$\text{HasFDerivAt}\left(\lambda y. \sum_n f_n(y)\right)\left(\sum_n f'_n(x)\right) x,$$$$
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 hasFDerivAt_tsum_of_isPreconnected (hu : Summable u) (hs : IsOpen s) (h's : IsPreconnected s)
(hf : ∀ n x, x ∈ s → HasFDerivAt (f n) (f' n x) x) (hf' : ∀ n x, x ∈ s → ‖f' n x‖ ≤ u n) (hx₀ : x₀ ∈ s)
(hf0 : Summable fun n => f n x₀) (hx : x ∈ s) : HasFDerivAt (fun y => ∑' n, f n y) (∑' n, f' n x) x := by
classical
have A : ∀ x : E, x ∈ s → Tendsto (fun t : Finset α => ∑ n ∈ t, f n x) atTop (𝓝 (∑' n, f n x)) :=
by
intro y hy
apply Summable.hasSum
exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf') (fun t y hy => ?_) A hx
exact HasFDerivAt.fun_sum fun n _ => hf n y hy
