English
If each f_i is C^N and there are uniform summable bounds on the derivatives up to order N, then the sum over i is C^N.
Русский
Если каждая функция f_i гладная до порядка N, и есть единые суммируемые пределы на все производные до N-го порядка, то сумма ∑ f_i является C^N.
LaTeX
$$$\text{If } f_i\in C^N\text{ for all }i,\text{ and }\exists\, v_k\ (k\le N)\text{ summable so that } \|D^k f_i\| ≤ v_k(i),\ \sum_i f_i\in C^N.$$$
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 converges everywhere on the set. -/
theorem summable_of_summable_hasFDerivAt_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 (f · x₀)) (hx : x ∈ s) : Summable fun n => f n x :=
by
haveI := Classical.decEq α
rw [summable_iff_cauchySeq_finset] at hf0 ⊢
have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i ∈ t, f' i x) atTop s :=
(tendstoUniformlyOn_tsum hu hf').uniformCauchySeqOn
refine cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i ∈ t, f i x) hs h's A (fun t y hy => ?_) hx₀ hx hf0
exact HasFDerivAt.fun_sum fun i _ => hf i y hy
