Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 00:37 e16e093e

View on Github →

feat(analysis/specific_limits): dirichlet and alternating series tests (#11908) Adds Dirichlet's test along with the alternating series test as a special case of the former. For the curious, Nick Bingham's course notes give some more context on Dirichlet's test. It's somewhat obscure.

Estimated changes

Modified docs/undergrad.yaml

Modified src/algebra/big_operators/intervals.lean

Modified src/analysis/normed/group/infinite_sum.lean

added theorem cauchy_seq_range_of_norm_bounded

Modified src/analysis/specific_limits.lean

added theorem antitone.cauchy_seq_alternating_series_of_tendsto_zero

added theorem antitone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded

added theorem antitone.tendsto_alternating_series_of_tendsto_zero

added theorem monotone.cauchy_seq_alternating_series_of_tendsto_zero

added theorem monotone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded

added theorem monotone.tendsto_alternating_series_of_tendsto_zero

added theorem norm_sum_neg_one_pow_le

Modified src/topology/uniform_space/cauchy.lean

modified def sequentially_complete.set_seq