English
If HasSum g a and for all i, ‖f i‖ ≤ g i, then ‖∑' i, f i‖ ≤ a.
Русский
Если ∑ g_i сходится к a и ‖f_i‖ ≤ g_i, тогда ‖∑ f_i‖ ≤ a.
LaTeX
$$$\\text{HasSum } g a \\land (\\forall i, \\|f(i)\\| ≤ g(i)) \\Rightarrow \\Bigl\\|\\sum' i, f(i)\\Bigr\\| ≤ 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_norm_bounded {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : HasSum g a) (h : ∀ i, ‖f i‖ ≤ g i) :
‖∑' i : ι, f i‖ ≤ a := by
by_cases hf : Summable f
· exact hf.hasSum.norm_le_of_bounded hg h
· rw [tsum_eq_zero_of_not_summable hf, norm_zero]
classical exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)
