Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-18 23:51 00d9f1de

View on Github →

feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171)

  • more material on infinite sums
  • minor fixes
  • cleanup
  • yury's comments

Estimated changes

modified theorem summable_iff_vanishing_norm
modified theorem summable_of_norm_bounded
added def option.cases_on'
modified theorem pmf.summable_coe
added theorem equiv.has_sum_iff
added theorem equiv.summable_iff
added theorem has_sum.add
added theorem has_sum.mul_left
added theorem has_sum.mul_right
added theorem has_sum.neg
added theorem has_sum.sigma
added theorem has_sum.sub
added theorem has_sum.summable
deleted theorem has_sum_add
deleted theorem has_sum_iff_of_summable
deleted theorem has_sum_mul_left
added theorem has_sum_mul_left_iff
deleted theorem has_sum_mul_right
added theorem has_sum_mul_right_iff
deleted theorem has_sum_neg
deleted theorem has_sum_of_has_sum
deleted theorem has_sum_sigma
deleted theorem has_sum_sub
deleted theorem has_sum_tsum
modified theorem has_sum_unique
deleted def option.cases_on'
added theorem summable.add
added theorem summable.has_sum
added theorem summable.has_sum_iff
added theorem summable.mul_left
added theorem summable.mul_right
added theorem summable.neg
added theorem summable.sigma'
added theorem summable.sigma
added theorem summable.sigma_factor
added theorem summable.sub
deleted theorem summable_add
deleted theorem summable_iff_cauchy
deleted theorem summable_mul_left
added theorem summable_mul_left_iff
deleted theorem summable_mul_right
added theorem summable_mul_right_iff
deleted theorem summable_neg
deleted theorem summable_sigma
deleted theorem summable_spec
deleted theorem summable_sub
modified theorem summable_zero
modified theorem tsum_eq_has_sum
added theorem tsum_le_tsum_of_inj
added theorem tsum_nonneg
added theorem tsum_nonpos
added theorem tsum_sigma'