W_le — Mathlib

English

For every natural number k, the Wallis sequence value W(k) does not exceed π/2.

Русский

Для каждого натурального k значение W(k) не превосходит π/2.

LaTeX

$$$\\forall k \\in \\mathbb{N},\\; W_k \\le \\frac{\\pi}{2}.$$$

Lean4

theorem W_le (k : ℕ) : W k ≤ π / 2 :=
  by
  rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
  rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
  apply integral_sin_pow_succ_le

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