English
Let Summable u and an open preconnected set t. Suppose g_n are differentiable on t with HasDerivAt(g_n, g'_n(y), y) and the derivatives are bounded by u_n. If the series ∑_n g_n(y0) converges at y0 ∈ t, then ∑_n g_n(y) converges for all y ∈ t.
Русский
Пусть сумма u суммируема и пусть t открыто и предсвязано. Пусть для каждой n функции g_n определены на t и имеют производную в точке y с помощью g'_n(y), причём ||g'_n(y)|| ≤ u_n. Если ∑_n g_n(y0) сходится в какой-либо y0 ∈ t, то ∑_n g_n(y) сходится для всех y ∈ t.
LaTeX
$$$$\sum_n u(n) < \infty\;\wedge\; IsOpen(t) \wedge IsPreconnected(t) \wedge (\forall n\, y\in t,\ HasDerivAt(g_n, g'_n(y), y)) \\ \wedge (\forall n\, y\in t,\ \|g'_n(y)\| \le u(n)) \\ \wedge (y_0 \in t) \wedge (Summable(\lambda n, g_n(y_0))) \Rightarrow (\forall y\in t, Summable(\lambda n, g_n(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 converges everywhere on the set. -/
theorem summable_of_summable_hasDerivAt_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 (g · y₀)) (hy : y ∈ t) : Summable fun n => g n y :=
by
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
refine summable_of_summable_hasFDerivAt_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
simpa
