norm_tsum_le_tsum_norm — Mathlib

English

If HasSum g a and ∥f i∥ ≤ g i for all i, then ∥∑' i, f i∥ ≤ a.

Русский

Если HasSum g a и ∥f_i∥ ≤ g_i, то ∥∑ f_i∥ ≤ a.

LaTeX

$$$\\text{HasSum } g a \\land (\\forall i, \\|f(i)\\| ≤ g(i)) \\Rightarrow \\|\\sum' i, f(i)\\| ≤ a$$$

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 norm_tsum_le_tsum_norm {f : ι → E} (hf : Summable fun i => ‖f i‖) : ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖ :=
  tsum_of_norm_bounded hf.hasSum fun _i => le_rfl

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