nnnorm_tsum_le — Mathlib

English

If the norm of f is eventually bounded by a summable real function g, then f is summable.

Русский

Если нормa f в конечном итоге ограничена суммируемой функцией g, то f суммируема.

LaTeX

$$$\\text{Summable } g \\land \\text{Eventually }(\\|f(i)\\| \\le g(i)) \\Rightarrow \\text{Summable } f$$$

Lean4

/-- If `∑' i, ‖f i‖₊` is summable, then `‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊`. Note that
we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
space. -/
theorem nnnorm_tsum_le {f : ι → E} (hf : Summable fun i => ‖f i‖₊) : ‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊ :=
  tsum_of_nnnorm_bounded hf.hasSum fun _i => le_rfl

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