Power series of arctangent

Statement

For every real $x$ with $|x| \le 1$, $$\arctan x = \sum_{n=0}^{\infty} \frac{(-1)^n x^{2n+1}}{2n + 1} = x - \frac{x^3}{3} + \frac{x^5}{5} - \cdots.$$

Remarks

For $|x| < 1$, integrate the geometric series $\frac{1}{1 + t^2} = \sum (-1)^n t^{2n}$ term by term from $0$ to $x$. Its sum is the derivative of arctangent. At $x = \pm 1$, the series converges by the alternating series test, and Abel's theorem gives the equality. At $x = 1$ this is the Leibniz formula $\pi/4 = 1 - 1/3 + 1/5 - \cdots$. The radius of convergence is $1$. Mathlib states the series for $|x| < 1$ as Real.hasSum_arctan.

Explanations

L1 human

The arctangent is a power series with odd powers and the simple coefficients $\pm 1/(2n+1)$. At $x = 1$, it gives a famous series for $\pi/4$.