English
If the norm is summable, then HasSum f a is equivalent to the partial sums ∑_{i< n} f(i) tending to a.
Русский
Если норма суммируема, то HasSum f a эквивалентно тому, что частичные суммы сходятся к a.
LaTeX
$$$\\text{Summable } \\|f\\| \\Rightarrow (\\text{HasSum } f a \\iff \\text{Tendsto } n \\mapsto \\sum_{i< n} f(i) \\to a)$$$
Lean4
/-- Quantitative result associated to the direct comparison test for series: If, 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_enorm_bounded {f : ι → ε} {g : ι → ℝ≥0∞} {a : ℝ≥0∞} (hg : HasSum g a) (h : ∀ i, ‖f i‖ₑ ≤ g i) :
‖∑' i : ι, f i‖ₑ ≤ a := by
by_cases hf : Summable f
· exact hf.hasSum.enorm_le_of_bounded hg h
· simp [tsum_eq_zero_of_not_summable hf]
