mathlib3
507c7ffc - feat(analysis/specific_limits): formula for `∑' n, n * r ^ n` (#5835)

Commit

4 years ago

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`.

Author

urkud

Parents