of_norm_le_summable_eventually — Mathlib

English

If u is summable and f_n x ≤ u_n eventually on cofinite sets, then HasSumUniformlyOn f (tsum_n f_n x) on s.

Русский

Если u суммируемо, и f_n x ≤ u_n почти повсюду на комплетах, то HasSumUniformlyOn f( tsum f_n x) на s.

LaTeX

$$$\\text{cofinite-eventually }(∥f_nx∥ ≤ u_n)\\Rightarrow \\text{HasSumUniformlyOn}(f, \\sum f_n, {s})$$$

Lean4

theorem of_norm_le_summable_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ} (hu : Summable u) {s : Set β}
    (hfu : ∀ᶠ n in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) : HasSumUniformlyOn f (fun x ↦ ∑' n, f n x) { s } := by
  simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum_of_cofinite_eventually hu hfu]

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