Commit 2023-03-09 18:34 e7e325c5

View on Github →

feat: port Analysis.Normed.Group.InfiniteSum (#2753)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/InfiniteSum.lean

added theorem HasSum.norm_le_of_bounded

added theorem cauchySeq_finset_iff_vanishing_norm

added theorem cauchySeq_finset_of_norm_bounded

added theorem cauchySeq_finset_of_norm_bounded_eventually

added theorem cauchySeq_finset_of_summable_norm

added theorem cauchySeq_range_of_norm_bounded

added theorem hasSum_iff_tendsto_nat_of_summable_norm

added theorem hasSum_of_subseq_of_summable

added theorem nnnorm_tsum_le

added theorem norm_tsum_le_tsum_norm

added theorem summable_iff_vanishing_norm

added theorem summable_of_nnnorm_bounded

added theorem summable_of_norm_bounded

added theorem summable_of_norm_bounded_eventually

added theorem summable_of_summable_nnnorm

added theorem summable_of_summable_norm

added theorem tsum_of_nnnorm_bounded

added theorem tsum_of_norm_bounded