English
Let k be a natural number and W_k denote the k-th Wallis term. Then a universal lower bound holds: ((2k+1)/(2k+2)) · (π/2) ≤ W_k.
Русский
Пусть k естественное число и W_k обозначает k-й член ряда Вальлиса. Тогда выполняется нижняя граница: ((2k+1)/(2k+2)) · (π/2) ≤ W_k.
LaTeX
$$$\frac{2k+1}{2k+2} \cdot \frac{\pi}{2} \le W_k$$$
Lean4
theorem le_W (k : ℕ) : ((2 : ℝ) * k + 1) / (2 * k + 2) * (π / 2) ≤ W k :=
by
rw [← le_div_iff₀ pi_div_two_pos, div_eq_inv_mul (W k) _]
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]
convert integral_sin_pow_succ_le (2 * k + 1)
rw [integral_sin_pow (2 * k)]
simp
