tendstoUniformly_tsum_of_cofinite_eventually

English

If a family f has summable sup-norm and the bound holds cofinitely for all x, the sum converges uniformly.

Русский

Если семейство f имеет суммируемую верхнюю границу по норме и это ограничение выполняется кофинифально почти для всех x, сумма сходится равномерно.

LaTeX

$$$\\text{tendstoUniformly_tsum_of_cofinite_eventually}$$$

Lean4

/-- An infinite sum of functions with eventually summable sup norm is the uniform limit of its
partial sums. Version with general index set. -/
theorem tendstoUniformly_tsum_of_cofinite_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ} (hu : Summable u)
    (hfu : ∀ᶠ (n : ι) in cofinite, ∀ x : β, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop :=
  by
  rw [← tendstoUniformlyOn_univ]
  apply tendstoUniformlyOn_tsum_of_cofinite_eventually hu
  simpa using hfu

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