English
For all x with |x| ≤ 1, the approximation error of cos x by 1 − x^2/2 is bounded by (5/96)|x|^4.
Русский
Для всех x с |x| ≤ 1 погрешность аппроксимации cos x через 1 − x^2/2 ограничена величиной (5/96)|x|^4.
LaTeX
$$$\\\\forall x \\\\in \\\\mathbb{R}, |x| \\\\le 1 \\\\Rightarrow \\\\left| \\\\cos x - \\left(1 - \\\\frac{x^2}{2}\\\\right) \\\\right| \\\\le |x|^4 \\\\left(\\\\frac{5}{96}\\\\right)$$$
Lean4
theorem cos_pos_of_le_one {x : ℝ} (hx : |x| ≤ 1) : 0 < cos x :=
calc
0 < 1 - x ^ 2 / 2 - |x| ^ 4 * (5 / 96) :=
sub_pos.2 <|
lt_sub_iff_add_lt.2
(calc
|x| ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2 :=
by
gcongr
· exact pow_le_one₀ (abs_nonneg _) hx
· rw [sq, ← abs_mul_self, abs_mul]
exact mul_le_one₀ hx (abs_nonneg _) hx
_ < 1 := by norm_num)
_ ≤ cos x := sub_le_comm.1 (abs_sub_le_iff.1 (cos_bound hx)).2
