Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 10:15 278a14b3

View on Github →

feat(analysis/p_series): prove the p-series convergence test (#4360)

Estimated changes

Modified docs/100.yaml

Created src/analysis/p_series.lean

added theorem ennreal.le_tsum_condensed

added theorem ennreal.tsum_condensed_le

added theorem finset.le_sum_condensed'

added theorem finset.le_sum_condensed

added theorem finset.sum_condensed_le'

added theorem finset.sum_condensed_le

added theorem nnreal.summable_condensed_iff

added theorem nnreal.summable_one_div_rpow

added theorem nnreal.summable_one_rpow_inv

added theorem real.not_summable_nat_cast_inv

added theorem real.not_summable_one_div_nat_cast

added theorem real.summable_nat_pow_inv

added theorem real.summable_nat_rpow_inv

added theorem real.summable_one_div_nat_pow

added theorem real.summable_one_div_nat_rpow

added theorem real.tendsto_sum_range_one_div_nat_succ_at_top

added theorem summable_condensed_iff_of_nonneg

Modified src/analysis/specific_limits.lean

deleted theorem half_le_harmonic_double_sub_harmonic

deleted def harmonic_series

deleted theorem harmonic_tendsto_at_top

deleted theorem mono_harmonic

deleted theorem self_div_two_le_harmonic_two_pow

Modified src/order/filter/cofinite.lean

added theorem filter.eventually_cofinite_ne