mul_le_sin — Mathlib

English

If 0 ≤ x ≤ π/2, then (2/π) x ≤ sin x.

Русский

Если 0 ≤ x ≤ π/2, то (2/π) x ≤ sin x.

LaTeX

$$$$ 0 \\le x \\le \\frac{\\pi}{2} \\Rightarrow \\frac{2}{\\pi} x \\le \\sin x. $$$$

Lean4

/-- One half of **Jordan's inequality**.

In the range `[0, π / 2]`, we have a linear lower bound on `sin`. The other half is given by
`Real.sin_le`.
-/
theorem mul_le_sin {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ π / 2) : 2 / π * x ≤ sin x :=
  by
  rw [← inv_div]
  simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
    @le_sin_mul ((π / 2)⁻¹ * x) (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
      (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])

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