tendstoUniformly_tsum — Mathlib

English

A tsum indexed by Nat with uniform bounds yields a uniform limit over all finite subsets.

Русский

Сумма, индексируемая по Нат, имеет равномерный предел по всем конечным подмножествам.

LaTeX

$$$\\text{tendstoUniformly_tsum_nat}$$$

Lean4

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with general index set. -/
theorem tendstoUniformly_tsum {f : α → β → F} (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun t : Finset α => fun x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop := by
  rw [← tendstoUniformlyOn_univ]; exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

Похожие утверждения