English
The real version of Euler’s sine product tends to sin(π x): as n→∞, π x ∏_{j< n} (1 - x^2/(j+1)^2) → sin(π x).
Русский
Реальная версия бесконечного продукта Эйлера для синуса стремится к sin(π x).
LaTeX
$$$\lim_{n\to\infty} π x \prod_{j=0}^{n-1} \left(1 - \frac{x^{2}}{(j+1)^{2}}\right) = \sin(π x)$$$
Lean4
/-- Euler's infinite product formula for the real sine function. -/
theorem _root_.Real.tendsto_euler_sin_prod (x : ℝ) :
Tendsto (fun n : ℕ => π * x * ∏ j ∈ Finset.range n, ((1 : ℝ) - x ^ 2 / ((j : ℝ) + 1) ^ 2)) atTop
(𝓝 <| sin (π * x)) :=
by
convert (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1
· ext1 n
rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]
suffices
(∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℂ) = (∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℝ) by
rw [this, Complex.ofReal_re]
rw [Complex.ofReal_prod]
refine Finset.prod_congr (by rfl) fun n _ => ?_
norm_cast
· rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]
