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.

source

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

source

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

source

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)

source

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)

source

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.

source

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.

source

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 Mathlib/Analysis/Real/Pi/Wallis.lean and other places.

source

theorem EulerSine.integral_cos_pow_pos (n : ℕ) :

0 < ∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ n

source

theorem EulerSine.sin_pi_mul_eq (z : ℂ) (n : ℕ) :

Complex.sin (↑Real.pi * z) = ((↑Real.pi * z * ∏ j ∈ Finset.range n, (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_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn.

source