Sequences and series

Find the sum of the first $20$ terms of the arithmetic sequence $5, 8, 11, 14, \dots$

Compute $3 + 6 + 12 + 24 + \dots + 3 \cdot 2^{9}$ (ten terms).

A sequence is defined by $a_1 = 2$ and $a_{n+1} = 3a_n - 1$. What is $a_5$?

Which of these infinite series converge? (Choose all that apply.)

Write $0.\overline{45} = 0.454545\ldots$ as a geometric series $a + ar + ar^2 + \cdots$ and find its sum $\tfrac pq$ in lowest terms. Enter $q$.

A student argues: "The terms $\tfrac{1}{\sqrt k}$ tend to $0$, so by the term test $\sum_{k=1}^{\infty} \tfrac{1}{\sqrt k}$ converges." What is wrong?

In the proof that the harmonic series diverges, why is $\tfrac{1}{9} + \tfrac{1}{10} + \dots + \tfrac{1}{16} \ge \tfrac12$?

In Lean, HasSum f S means "the series $\sum_{n \ge 0} f(n)$ converges to $S$". Which statement formalises $0.999\ldots = 1$?

Write terms_needed(a, r, eps) for $0 < r < 1$ and $a > 0$: the smallest $n$ such that the partial sum $S_n = a + ar + \dots + ar^{n-1}$ is within eps of the limit $\tfrac{a}{1 - r}$. Use Fraction for exact arithmetic (the tests pass fractions). By Theorem 5 the gap is $\tfrac{a\,r^n}{1 - r}$.