# Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

# Euler's infinite product for the sine function #

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][salwinski2018]: 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 EulerSine.antideriv_cos_comp_const_mul {z : } (hz : z 0) (x : ) :
HasDerivAt (fun y => Complex.sin (2 * z * y) / (2 * z)) (Complex.cos (2 * z * x)) x
theorem EulerSine.antideriv_sin_comp_const_mul {z : } (hz : z 0) (x : ) :
HasDerivAt (fun y => -Complex.cos (2 * z * y) / (2 * z)) (Complex.sin (2 * z * x)) x
theorem EulerSine.integral_cos_mul_cos_pow_aux {z : } {n : } (hn : 2 n) (hz : z 0) :
∫ (x : ) in 0 .., Complex.cos (2 * z * x) * ↑() ^ n = n / (2 * z) * ∫ (x : ) in 0 .., Complex.sin (2 * z * x) * ↑() * ↑() ^ (n - 1)
theorem EulerSine.integral_sin_mul_sin_mul_cos_pow_eq {z : } {n : } (hn : 2 n) (hz : z 0) :
∫ (x : ) in 0 .., Complex.sin (2 * z * x) * ↑() * ↑() ^ (n - 1) = (n / (2 * z) * ∫ (x : ) in 0 .., Complex.cos (2 * z * x) * ↑() ^ n) - (n - 1) / (2 * z) * ∫ (x : ) in 0 .., Complex.cos (2 * z * x) * ↑() ^ (n - 2)
theorem EulerSine.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) * ↑() ^ n = (n - 1) / n * ∫ (x : ) in 0 .., Complex.cos (2 * z * x) * ↑() ^ (n - 2)

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

theorem EulerSine.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) * ↑() ^ (2 * n + 2) = (2 * n + 1) / (2 * n + 2) * ∫ (x : ) in 0 .., Complex.cos (2 * z * x) * ↑() ^ (2 * n)

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

theorem EulerSine.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 EulerSine.integral_cos_pow_pos (n : ) :
0 < ∫ (x : ) in 0 .., ^ n
theorem EulerSine.sin_pi_mul_eq (z : ) (n : ) :
Complex.sin ( * z) = (( * z * Finset.prod () fun j => 1 - z ^ 2 / (j + 1) ^ 2) * ∫ (x : ) in 0 .., Complex.cos (2 * z * 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_isCompact_of_continuousOn.

theorem EulerSine.tendsto_integral_cos_pow_mul_div {f : } (hf : ContinuousOn f (Set.Icc 0 ())) :
Filter.Tendsto (fun n => (∫ (x : ) in 0 .., ↑() ^ n * f x) / ↑(∫ (x : ) in 0 .., ^ n)) Filter.atTop (nhds (f 0))
theorem Complex.tendsto_euler_sin_prod (z : ) :
Filter.Tendsto (fun n => * z * Finset.prod () fun j => 1 - z ^ 2 / (j + 1) ^ 2) Filter.atTop (nhds (Complex.sin ( * z)))

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

theorem Real.tendsto_euler_sin_prod (x : ) :
Filter.Tendsto (fun n => * Finset.prod () fun j => 1 - x ^ 2 / (j + 1) ^ 2) Filter.atTop (nhds (Real.sin ()))

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