English
An infinite sum of functions with summable sup-norm is the uniform limit of its finite partial sums over any index set, provided the sup-norm bounds are summable.
Русский
Бесконечная сумма функции с суммируемой верхней гранью нормы равномерно сходится к сумме по любому индексу.
LaTeX
$$$\\text{TendstoUniformlyOn}_s\\big( \\sum_{n\\in t} f(n,\\cdot) \\big) (\\sum_{n} f(n,\\cdot))$ for appropriate conditions.$$
Lean4
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version relative to a set, with general index set. -/
theorem tendstoUniformlyOn_tsum {f : α → β → F} (hu : Summable u) {s : Set β} (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
TendstoUniformlyOn (fun t : Finset α => fun x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop s :=
by
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx
have A : Summable fun n => ‖f n x‖ := .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n => hfu n x hx) hu
rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl t, add_sub_cancel_left]
apply lt_of_le_of_lt _ ht
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
exact (A.subtype _).tsum_le_tsum (fun n => hfu _ _ hx) (hu.subtype _)
