sin_div_le_inv_abs — Mathlib

English

For all real x, sin x / x ≤ |x|^{-1}. In particular, for x ≠ 0, sin x / x ≤ 1/|x|.

Русский

Для любых действительных x верно: sin x / x ≤ |x|^{-1}. В частности, при x ≠ 0: sin x / x ≤ 1/|x|.

LaTeX

$$$\dfrac{\sin x}{x} \le |x|^{-1} \quad\text{for } x \neq 0$$$

Lean4

theorem sin_div_le_inv_abs (x : ℝ) : sin x / x ≤ |x|⁻¹ :=
  by
  rcases lt_trichotomy x 0 with hx | rfl | hx
  · rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]
    · ring_nf
      rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]
      exact neg_one_le_sin x
    · simpa using hx
  · simp
  · rw [abs_of_nonneg hx.le, div_eq_mul_inv, mul_inv_le_iff₀ hx, inv_mul_cancel₀ hx.ne']
    exact sin_le_one x

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