English
Complex version of Euler’s sine product tends to sin(π z): as n→∞, π z ∏_{j< n} (1 - z^2/(j+1)^2) tends to sin(π z).
Русский
Комплексная версия бесконечного продукта Эйлера для синуса стремится к sin(π z): предел равен sin(π z).
LaTeX
$$$\lim_{n\to\infty} π z \prod_{j=0}^{n-1} (1 - z^{2}/(j+1)^{2}) = \sin(π z)$$$
Lean4
/-- Euler's infinite product formula for the complex sine function. -/
theorem _root_.Complex.tendsto_euler_sin_prod (z : ℂ) :
Tendsto (fun n : ℕ => π * z * ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)) atTop
(𝓝 <| Complex.sin (π * z)) :=
by
have A :
Tendsto
(fun n : ℕ =>
((π * z * ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)) *
∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)) /
(∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n) : ℝ))
atTop (𝓝 <| _) :=
Tendsto.congr (fun n => sin_pi_mul_eq z n) tendsto_const_nhds
have : 𝓝 (Complex.sin (π * z)) = 𝓝 (Complex.sin (π * z) * 1) := by rw [mul_one]
simp_rw [this, mul_div_assoc] at A
convert (tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A
suffices
Tendsto
(fun n : ℕ =>
(∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) / (∫ x in (0 : ℝ)..π / 2, cos x ^ n : ℝ))
atTop (𝓝 1)
from this.comp (tendsto_id.const_mul_atTop' zero_lt_two)
have : ContinuousOn (fun x : ℝ => Complex.cos (2 * z * x)) (Icc 0 (π / 2)) :=
(Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).continuousOn
convert tendsto_integral_cos_pow_mul_div this using 1
· ext1 n; congr 2 with x : 1; rw [mul_comm]
· rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]
