k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
no goals
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
rfl