feat(*): a few more tests for `summable`, docstrings (#4325)
### Important new theorems:
* `summable_geometric_iff_norm_lt_1`: a geometric series in a normed field is summable iff the norm of the common ratio is less than 1;
* `summable.tendsto_cofinite_zero`: divergence test: if `f` is a `summable` function, then `f x` tends to zero along `cofinite`;
### API change
* rename `cauchy_seq_of_tendsto_nhds` to `filter.tendsto.cauchy_seq` to enable dot syntax.
