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: 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 * ∏ 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.

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 * ∏ j ∈ Finset.range n, (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 * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) Filter.atTop (nhds (Real.sin (Real.pi * x)))

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