Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-01 09:16 9c241b0d

View on Github →

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.

Estimated changes

added theorem summable.vanishing
modified theorem nnreal.summable_of_le
modified theorem nnreal.tendsto_sum_nat_add