Commit 2024-03-16 15:45 1e2c4067

View on Github →

feat(InfiniteSum/NatInt): lemmas on sums over ℤ (#11069) This PR combines several results involving topological sums over ℤ. These results are used in #10011 (Hurwitz zeta functions) where sums over ℤ feature heavily.

  • Fill in tsum and Summable variants for lemmas proved for HasSum
  • Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme
  • Generalise several lemmas to allow the target space to be a topological monoid rather than a group.
  • Speed up some slow proofs (the old summable_int_of_summable_nat took about 10s to compile on my machine, its replacement Summable.of_nat_of_neg is 1000 times faster)

Estimated changes

modified theorem HasSum.even_add_odd
modified theorem HasSum.int_rec
added theorem HasSum.nat_add_neg
deleted theorem HasSum.nonneg_add_neg
added theorem HasSum.of_nat_of_neg
deleted theorem HasSum.sum_nat_of_sum_int
modified theorem HasSum.sum_range_add
modified theorem HasSum.tendsto_sum_nat
added theorem HasSum.zero_add
added theorem Summable.comp_nat_add
added theorem Summable.even_add_odd
added theorem Summable.int_rec
added theorem Summable.nat_add_neg
added theorem Summable.of_nat_of_neg
modified theorem hasSum_nat_add_iff'
modified theorem hasSum_nat_add_iff
modified theorem rel_iSup_sum
modified theorem rel_iSup_tsum
modified theorem rel_sup_add
modified theorem sum_add_tsum_nat_add
modified theorem summable_nat_add_iff
modified theorem tendsto_sum_nat_add
modified theorem tsum_eq_zero_add
modified theorem tsum_even_add_odd
modified theorem tsum_iSup_decode₂
modified theorem tsum_iUnion_decode₂
added theorem tsum_int_rec
added theorem tsum_nat_add_neg
added theorem tsum_of_nat_of_neg