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 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos x) ^ n = n / (2 * z) * ∫ (x : ) in 0 ..Real.pi / 2, Complex.sin (2 * z * x) * (Real.sin x) * (Real.cos x) ^ (n - 1)
theorem EulerSine.integral_sin_mul_sin_mul_cos_pow_eq {z : } {n : } (hn : 2 n) (hz : z 0) :
∫ (x : ) in 0 ..Real.pi / 2, Complex.sin (2 * z * x) * (Real.sin x) * (Real.cos x) ^ (n - 1) = (n / (2 * z) * ∫ (x : ) in 0 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos x) ^ n) - (n - 1) / (2 * z) * ∫ (x : ) in 0 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos 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 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos x) ^ n = (n - 1) / n * ∫ (x : ) in 0 ..Real.pi / 2, 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 EulerSine.integral_cos_mul_cos_pow_even {z : } (n : ) (hz : z 0) :
(1 - z ^ 2 / (n + 1) ^ 2) * ∫ (x : ) in 0 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos x) ^ (2 * n + 2) = (2 * n + 1) / (2 * n + 2) * ∫ (x : ) in 0 ..Real.pi / 2, 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 EulerSine.integral_cos_pow_eq (n : ) :
∫ (x : ) in 0 ..Real.pi / 2, Real.cos x ^ n = 1 / 2 * ∫ (x : ) in 0 ..Real.pi, Real.sin x ^ 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 ..Real.pi / 2, Real.cos x ^ n
theorem EulerSine.sin_pi_mul_eq (z : ) (n : ) :
Complex.sin (Real.pi * z) = ((Real.pi * z * Finset.prod (Finset.range n) fun (j : ) => 1 - z ^ 2 / (j + 1) ^ 2) * ∫ (x : ) in 0 ..Real.pi / 2, Complex.cos (2 * z * x) * (Real.cos x) ^ (2 * n)) / (∫ (x : ) in 0 ..Real.pi / 2, Real.cos x ^ (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 (Real.pi / 2))) :
Filter.Tendsto (fun (n : ) => (∫ (x : ) in 0 ..Real.pi / 2, (Real.cos x) ^ n * f x) / (∫ (x : ) in 0 ..Real.pi / 2, Real.cos x ^ n)) Filter.atTop (nhds (f 0))
theorem Complex.tendsto_euler_sin_prod (z : ) :
Filter.Tendsto (fun (n : ) => Real.pi * z * Finset.prod (Finset.range n) fun (j : ) => 1 - z ^ 2 / (j + 1) ^ 2) Filter.atTop (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 (fun (n : ) => Real.pi * x * Finset.prod (Finset.range n) fun (j : ) => 1 - x ^ 2 / (j + 1) ^ 2) Filter.atTop (nhds (Real.sin (Real.pi * x)))

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