Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 21:34 2ab63a02

View on Github →

feat(topology/algebra/infinite_sum, analysis/normed_space/basic): product of two tsums, cauchy product (#8445)

Estimated changes

Modified src/analysis/normed_space/basic.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 src/data/finset/nat_antidiagonal.lean

added def finset.nat.sigma_antidiagonal_equiv_prod

Modified src/topology/algebra/infinite_sum.lean

added theorem has_sum.mul

added theorem has_sum.mul_eq

added theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal

added theorem summable_sum_mul_antidiagonal_of_summable_mul

added theorem summable_sum_mul_range_of_summable_mul

added theorem tsum_mul_tsum

added theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal

added theorem tsum_mul_tsum_eq_tsum_sum_range

Modified src/topology/instances/ennreal.lean

added theorem summable_of_sum_le