Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-25 01:08 507c7ffc

View on Github →

feat(analysis/specific_limits): formula for ∑' n, n * r ^ n (#5835) Also prove that ∑' n, n ^ k * r ^ n is summable for any k : ℕ, ∥r∥ < 1.

Estimated changes

Modified src/algebra/group_with_zero/basic.lean

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_O.pow

modified theorem asymptotics.is_O_bot

added theorem asymptotics.is_O_with.pow'

added theorem asymptotics.is_O_with.pow

modified theorem asymptotics.is_O_with_bot

added theorem asymptotics.is_o.pow

modified theorem asymptotics.is_o_bot

added theorem summable_of_is_O

added theorem summable_of_is_O_nat

Modified src/analysis/normed_space/basic.lean

added theorem nat.norm_cast_le

Modified src/analysis/special_functions/exp_log.lean

Modified src/analysis/specific_limits.lean

added theorem has_sum_coe_mul_geometric_of_norm_lt_1

added theorem is_o_coe_const_pow_of_one_lt

added theorem is_o_pow_const_const_pow_of_one_lt

added theorem is_o_pow_const_mul_const_pow_const_pow_of_norm_lt

added theorem summable_norm_pow_mul_geometric_of_norm_lt_1

added theorem summable_pow_mul_geometric_of_norm_lt_1

added theorem tendsto_pow_const_div_const_pow_of_one_lt

added theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one

added theorem tsum_coe_mul_geometric_of_norm_lt_1

Modified src/data/nat/basic.lean

added theorem nat.rec_add_one

added theorem nat.rec_zero

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/instances/ennreal.lean

added theorem ennreal.nhds_within_Ioi_coe_ne_bot

added theorem ennreal.nhds_within_Ioi_zero_ne_bot