---
tag: DQEHD56649
kind: statement
role: theorem
name: Euler's sine product
msc: [30D10, 40A20]
uses: [0A7YDKRNR6, 0419794R0T, ACSF58HYDH, 08FPABDQ4C]
about: [00NZKRSWNX]
sources:
  - url: https://en.wikipedia.org/wiki/Basel_problem
---

## Statement

For every $z \in \C$,
$$\sin(\pi z) = \pi z \prod_{n=1}^{\infty} \left(1 - \frac{z^2}{n^2}\right),$$
where $\sin$ is the [[complex sine|0A7YDKRNR6]].
The product converges absolutely for every $z$, and [[uniformly|08FPABDQ4C]] on each compact subset of $\C$.

## Remarks

The convergence follows from $\sum_n \abs{z}^2 / n^2 < \infty$.
Both sides are [[entire functions|0419794R0T]] with simple zeros exactly at the integers.
By the [[Weierstrass factorization theorem|11VC51YHQJ]], their quotient is $e^{g(z)}$ for an entire function $g$.
One shows that $g$ is constant, for example by comparing logarithmic derivatives with the partial fraction expansion $\pi \cot(\pi z) = \frac{1}{z} + \sum_{n \ge 1} \frac{2z}{z^2 - n^2}$; the limit at $z = 0$ then gives $e^{g} = 1$.
Comparing the coefficients of $z^3$ on both sides gives $\sum_{n \ge 1} 1/n^2 = \pi^2/6$, the [[Basel problem|0DMY75D6FV]].
At $z = 1/2$ it gives the [[Wallis product|0XCYA4YERS]] $\frac{2}{\pi} = \prod_{n \ge 1} \left(1 - \frac{1}{4n^2}\right)$.
In Mathlib it is `Complex.tendsto_euler_sin_prod`.

## Explanations

### L1 human

A polynomial is determined, up to a constant, by its roots.
The sine function behaves like a polynomial of infinite degree with roots at all the integers.
Euler's formula writes $\sin(\pi z)$ as the product of the factors $(1 - z/n)(1 + z/n)$ over all its roots, times $\pi z$.

### L2 human

The formula is the standard example of a [[Weierstrass product|ACSF58HYDH]].
Here no exponential correction factors are needed, because the factors $1 - z/n$ and $1 + z/n$ are paired.
Taking the logarithmic derivative gives the partial fraction expansion of $\pi\cot(\pi z)$.
Combined with the product for $1/\Gamma$, it yields the [[reflection formula|WF7KQAQTS2]] for the gamma function.