k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
k : ℕ
⊢ W k ≤ π / 2
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
k : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
no goals
k : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
apply integral_sin_pow_succ_le