Commit 2023-05-25 19:41 3dde1ee7

View on Github →

feat: port Analysis.PSeries (#4182) Removed the simp attribute on one lemma because simpNF was timing out trying to reduce the LHS. See Zulip for the problem. Once this error is corrected with simp, we should be able to add the attribute again.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/PSeries.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_rpow

added theorem NNReal.summable_rpow_inv

added theorem Real.not_summable_nat_cast_inv

added theorem Real.not_summable_one_div_nat_cast

added theorem Real.summable_abs_int_rpow

added theorem Real.summable_nat_pow_inv

added theorem Real.summable_nat_rpow

added theorem Real.summable_nat_rpow_inv

added theorem Real.summable_one_div_int_pow

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_atTop

added theorem sum_Ioc_inv_sq_le_sub

added theorem sum_Ioo_inv_sq_le

added theorem summable_condensed_iff_of_nonneg