tendstoUniformly_tsum_nat — Mathlib

English

With cofinite eventual bounds, the tsum converges uniformly to tsum across all x.

Русский

С учетом кофинитных условий сумма сходится равномерно к сумме по всем x.

LaTeX

$$$\\text{tendstoUniformly_tsum_nat_eventually}$$$

Lean4

/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with index set `ℕ`. -/
theorem tendstoUniformly_tsum_nat {f : ℕ → β → F} {u : ℕ → ℝ} (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun N => fun x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' n, f n x) atTop := fun v hv =>
  tendsto_finset_range.eventually (tendstoUniformly_tsum hu hfu v hv)

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