Commit 2023-03-14 07:53 c88ae7e9

View on Github →

feat: port Analysis.Normed.Field.InfiniteSum (#2860)

Estimated changes

Modified Mathlib.lean

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

added theorem Summable.mul_norm

added theorem Summable.mul_of_nonneg

added theorem summable_mul_of_summable_norm

added theorem summable_norm_sum_mul_antidiagonal_of_summable_norm

added theorem summable_norm_sum_mul_range_of_summable_norm

added theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm

added theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm

added theorem tsum_mul_tsum_of_summable_norm

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem summable_prod_of_nonneg