English
An indexed family of functions with summable upper bounds yields a uniform limit of its partial sums when indexed by natural numbers.
Русский
Семейство функций с суммируемыми верхними границами приводит к равномерной предельной сумме частичных сумм по натовым индексам.
LaTeX
$$$\\text{TendstoUniformlyOn}_{\\mathbb{N}}(\\text{partial sums}) = \\text{tsum}$$$
Lean4
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with index set `ℕ`. -/
theorem tendstoUniformlyOn_tsum_nat {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) {s : Set β}
(hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
TendstoUniformlyOn (fun N => fun x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' n, f n x) atTop s := fun v hv =>
tendsto_finset_range.eventually (tendstoUniformlyOn_tsum hu hfu v hv)
