Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-23 15:54 6c092955

View on Github →

feat(analysis/specific_limits): basic ratio test for summability of a nat-indexed family (#7277)

Estimated changes

Modified src/analysis/specific_limits.lean

added theorem le_geom

added theorem lt_geom

added theorem not_summable_of_ratio_norm_eventually_ge

added theorem not_summable_of_ratio_test_tendsto_gt_one

added theorem summable_of_ratio_norm_eventually_le

added theorem summable_of_ratio_test_tendsto_lt_one