mul_abs_le_abs_sin — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Half of **Jordan's inequality** for absolute values. -/
theorem mul_abs_le_abs_sin (hx : |x| ≤ π / 2) : 2 / π * |x| ≤ |sin x| :=
  by
  wlog hx₀ : 0 ≤ x
  case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀
  rw [abs_of_nonneg hx₀] at hx ⊢
  exact (mul_le_sin hx₀ hx).trans (le_abs_self _)

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