of_norm_le_summable — Mathlib

English

If u is summable and |f_n x| ≤ u_n for all n and x in s, then HasSumUniformlyOn f (tsum_n f_n) on s.

Русский

Если u суммируемо, и |f_n x| ≤ u_n для всех n и x в s, то HasSumUniformlyOn f( tsum_n f_n ) на s.

LaTeX

$$$\\text{Summable }u \\;\\rightarrow\\; \\{s\\} \\Rightarrow\\ HasSumUniformlyOn f (\\sum' n, f_n x) {s}$$$

Lean4

theorem of_norm_le_summable {f : α → β → F} (hu : Summable u) {s : Set β} (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
    HasSumUniformlyOn f (fun x ↦ ∑' n, f n x) { s } := by
  simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum hu hfu]

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