Infinite sums in (semi)normed groups #
In a complete (semi)normed group,
-
summable_iff_vanishing_norm
: a series∑' i, f i
is summable if and only if for anyε > 0
, there exists a finite sets
such that the sum∑ i in t, f i
over any finite sett
disjoint withs
has norm less thanε
; -
summable_of_norm_bounded
,summable_of_norm_bounded_eventually
: if∥f i∥
is bounded above by a summable series∑' i, g i
, then∑' i, f i
is summable as well; the same is true if the inequality hold only off some finite set. -
tsum_of_norm_bounded
,has_sum.norm_le_of_bounded
: if∥f i∥ ≤ g i
, where∑' i, g i
is a summable series, then∥∑' i, f i∥ ≤ ∑' i, g i
.
Tags #
infinite series, absolute convergence, normed group
A version of the direct comparison test for conditionally convergent series.
See cauchy_seq_finset_of_norm_bounded
for the same statement about absolutely convergent ones.
If a function f
is summable in norm, and along some sequence of finsets exhausting the space
its sum is converging to a limit a
, then this holds along all finsets, i.e., f
is summable
with sum a
.
The direct comparison test for series: if the norm of f
is bounded by a real function g
which is summable, then f
is summable.
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.
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.
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.
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.
Variant of the direct comparison test for series: if the norm of f
is eventually bounded by a
real function g
which is summable, then f
is summable.