# mathlib3documentation

analysis.special_functions.trigonometric.euler_sine_prod

# Euler's infinite product for the sine function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the infinite product formula

$$\sin \pi z = \pi z \prod_{n = 1}^\infty \left(1 - \frac{z ^ 2}{n ^ 2}\right)$$

for any real or complex z. Our proof closely follows the article Salwinski, Euler's Sine Product Formula: An Elementary Proof: the basic strategy is to prove a recurrence relation for the integrals ∫ x in 0..π/2, cos 2 z x * cos x ^ (2 * n), generalising the arguments used to prove Wallis' limit formula for π.

## Recursion formula for the integral of cos (2 * z * x) * cos x ^ n#

We evaluate the integral of cos (2 * z * x) * cos x ^ n, for any complex z and even integers n, via repeated integration by parts.

theorem euler_sine.antideriv_cos_comp_const_mul {z : } (hz : z 0) (x : ) :
has_deriv_at (λ (y : ), complex.sin (2 * z * y) / (2 * z)) (complex.cos (2 * z * x)) x
theorem euler_sine.antideriv_sin_comp_const_mul {z : } (hz : z 0) (x : ) :
has_deriv_at (λ (y : ), -complex.cos (2 * z * y) / (2 * z)) (complex.sin (2 * z * x)) x
theorem euler_sine.integral_cos_mul_cos_pow_aux {z : } {n : } (hn : 2 n) (hz : z 0) :
(x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ n = n / (2 * z) * (x : ) in 0.., complex.sin (2 * z * x) * (real.sin x) * (real.cos x) ^ (n - 1)
theorem euler_sine.integral_sin_mul_sin_mul_cos_pow_eq {z : } {n : } (hn : 2 n) (hz : z 0) :
(x : ) in 0.., complex.sin (2 * z * x) * (real.sin x) * (real.cos x) ^ (n - 1) = (n / (2 * z) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ n) - (n - 1) / (2 * z) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ (n - 2)
theorem euler_sine.integral_cos_mul_cos_pow {z : } {n : } (hn : 2 n) (hz : z 0) :
(1 - 4 * z ^ 2 / n ^ 2) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ n = (n - 1) / n * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ (n - 2)

Note this also holds for z = 0, but we do not need this case for sin_pi_mul_eq.

theorem euler_sine.integral_cos_mul_cos_pow_even {z : } (n : ) (hz : z 0) :
(1 - z ^ 2 / (n + 1) ^ 2) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ (2 * n + 2) = (2 * n + 1) / (2 * n + 2) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ (2 * n)

Note this also holds for z = 0, but we do not need this case for sin_pi_mul_eq.

theorem euler_sine.integral_cos_pow_eq (n : ) :
(x : ) in 0.., ^ n = 1 / 2 * (x : ) in 0..real.pi, ^ n

Relate the integral cos x ^ n over [0, π/2] to the integral of sin x ^ n over [0, π], which is studied in data.real.pi.wallis and other places.

theorem euler_sine.integral_cos_pow_pos (n : ) :
0 < (x : ) in 0.., ^ n
theorem euler_sine.sin_pi_mul_eq (z : ) (n : ) :
complex.sin (real.pi * z) = * (finset.range n).prod (λ (j : ), 1 - z ^ 2 / (j + 1) ^ 2) * (x : ) in 0.., complex.cos (2 * z * x) * (real.cos x) ^ (2 * n)) / (x : ) in 0.., ^ (2 * n)

Finite form of Euler's sine product, with remainder term expressed as a ratio of cosine integrals.

## Conclusion of the proof #

The main theorem complex.tendsto_euler_sin_prod, and its real variant real.tendsto_euler_sin_prod, now follow by combining sin_pi_mul_eq with a lemma stating that the sequence of measures on [0, π/2] given by integration against cos x ^ n (suitably normalised) tends to the Dirac measure at 0, as a special case of the general result tendsto_set_integral_pow_smul_of_unique_maximum_of_is_compact_of_continuous_on.

theorem euler_sine.tendsto_integral_cos_pow_mul_div {f : } (hf : (set.Icc 0 (real.pi / 2))) :
filter.tendsto (λ (n : ), ( (x : ) in 0.., (real.cos x) ^ n * f x) / (x : ) in 0.., ^ n) filter.at_top (nhds (f 0))
theorem complex.tendsto_euler_sin_prod (z : ) :
filter.tendsto (λ (n : ), * (finset.range n).prod (λ (j : ), 1 - z ^ 2 / (j + 1) ^ 2)) filter.at_top (nhds (complex.sin (real.pi * z)))

Euler's infinite product formula for the complex sine function.

theorem real.tendsto_euler_sin_prod (x : ) :
filter.tendsto (λ (n : ), * (finset.range n).prod (λ (j : ), 1 - x ^ 2 / (j + 1) ^ 2)) filter.at_top (nhds (real.sin (real.pi * x)))

Euler's infinite product formula for the real sine function.