W_eq_integral_sin_pow_div_integral_sin_pow

English

The normalized Wallis product relates to a ratio of integrals of powers of sine over [0, π].

Русский

Нормализованное произведение Уоллиса связано с отношением интегралов степеней синуса на [0, π].

LaTeX

$$$\\left( \\frac{\\pi}{2} \\right)^{-1} W(k) = \\frac{\\displaystyle \\int_{0}^{\\pi} \\sin^{2k+1} x \\, dx}{\\displaystyle \\int_{0}^{\\pi} \\sin^{2k} x \\, dx}$$$

Lean4

theorem W_eq_integral_sin_pow_div_integral_sin_pow (k : ℕ) :
    (π / 2)⁻¹ * W k = (∫ x : ℝ in 0..π, sin x ^ (2 * k + 1)) / ∫ x : ℝ in 0..π, sin x ^ (2 * k) :=
  by
  rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
  simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
  rfl

Похожие утверждения