tendstoUniformlyOn_tsum_nat_eventually

English

If the sup-norm bounds are summable and hold eventually for natural indices, the tsum is a uniform limit of finite sums on all sets.

Русский

Если верхние границы нормы суммируемы и выполняются почти постоянно, то ∑n f_n убивает равномерно.

LaTeX

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

Lean4

theorem tendstoUniformlyOn_tsum_nat_eventually {α F : Type*} [NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → α → F}
    {u : ℕ → ℝ} (hu : Summable u) {s : Set α} (hfu : ∀ᶠ n in atTop, ∀ x ∈ s, ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun N 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_of_cofinite_eventually hu (Nat.cofinite_eq_atTop ▸ hfu) v hv

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