Sine and cosine

Definition

The sine and cosine functions $\sin, \cos \colon \mathbb{R} \to \mathbb{R}$ are defined by the power series $$\sin x = \sum_{n=0}^{\infty} \frac{(-1)^n x^{2n+1}}{(2n+1)!}, \qquad \cos x = \sum_{n=0}^{\infty} \frac{(-1)^n x^{2n}}{(2n)!}.$$

Remarks

Both series converge absolutely for every real $x$. Sine is odd and cosine is even. Also $\sin 0 = 0$ and $\cos 0 = 1$. Geometrically, $(\cos x, \sin x)$ is the point of the unit circle at arc length $x$ from $(1, 0)$, counterclockwise. Mathlib defines Real.sin and Real.cos from the complex exponential, with $\cos x + i \sin x = e^{i x}$.

Explanations

L1 human

Sine and cosine describe motion around the unit circle. In analysis, we define them by power series, and we then prove their geometric properties.