English
For 0 < x ≤ 1, x − x^3/4 < sin x.
Русский
Пусть 0 < x ≤ 1. Тогда x − x^3/4 < sin x.
LaTeX
$$$0 < x \le 1 \Rightarrow x - \dfrac{x^3}{4} < \sin x$$$
Lean4
/-- For 0 < x ≤ 1 we have x - x ^ 3 / 4 < sin x.
This is also true for x > 1, but it's nontrivial for x just above 1. This inequality is not
tight; the tighter inequality is sin x > x - x ^ 3 / 6 for all x > 0, but this inequality has
a simpler proof. -/
theorem sin_gt_sub_cube {x : ℝ} (h : 0 < x) (h' : x ≤ 1) : x - x ^ 3 / 4 < sin x :=
by
have hx : |x| = x := abs_of_nonneg h.le
have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
rw [le_sub_iff_add_le, hx] at this
refine lt_of_lt_of_le ?_ this
have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by norm_num [div_eq_mul_inv, ← mul_sub]
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)
apply pow_le_pow_of_le_one h.le h'
simp
