English
Euler's infinite product for sine: the limit of π z ∏_{j< n} (1 - z^2/(j+1)^2) as n→∞ equals sin(π z).
Русский
Бесконечный продукт Эйлера для синуса: предел произведения ∏ (1 - z^2/(j+1)^2) умноженного на π z стремится к sin(π z).
LaTeX
$$$\lim_{n\to\infty} \pi z \prod_{j=0}^{n-1} \left(1 - \frac{z^{2}}{(j+1)^{2}}\right) = \sin(\pi z)$$$
Lean4
/-- Finite form of Euler's sine product, with remainder term expressed as a ratio of cosine
integrals. -/
theorem sin_pi_mul_eq (z : ℂ) (n : ℕ) :
Complex.sin (π * z) =
((π * 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) : ℝ) :=
by
rcases eq_or_ne z 0 with (rfl | hz)
· simp
induction n with
| zero =>
simp_rw [mul_zero, pow_zero, mul_one, Finset.prod_range_zero, mul_one, integral_one, sub_zero]
rw [integral_cos_mul_complex (mul_ne_zero two_ne_zero hz), Complex.ofReal_zero, mul_zero, Complex.sin_zero,
zero_div, sub_zero, (by push_cast; field_simp : 2 * z * ↑(π / 2) = π * z)]
simp [field]
| succ n hn =>
rw [hn, Finset.prod_range_succ]
set A := ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C :=
by
rw [integral_cos_pow_eq]
dsimp only [C]
rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ', zero_mul, zero_mul, zero_mul,
sub_zero, zero_div, zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
rw [this]
change
π * z * A * B / C =
(π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) /
((2 * n + 1) / (2 * n + 2) * C : ℝ)
have :
(π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
π * z * A *
(((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) :=
by grind
rw [this]
suffices
(((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
(2 * n + 1) / (2 * n + 2) * B
by
rw [this, Complex.ofReal_mul, Complex.ofReal_div]
have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
have : 2 * (n : ℂ) + 1 ≠ 0 :=
by
convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
simp
have : (n : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
simp [field]
convert integral_cos_mul_cos_pow_even n hz
rw [Nat.cast_succ]
