English
If HasSum g a and ∥f i∥ ≤ g 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
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
summable, and for all `i`, `‖f i‖₊ ≤ g i`, then `‖∑' i, f i‖₊ ≤ ∑' i, g 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 tsum_of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : HasSum g a) (h : ∀ i, ‖f i‖₊ ≤ g i) :
‖∑' i : ι, f i‖₊ ≤ a :=
by
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *
exact tsum_of_norm_bounded hg h
