English
If |x| ≤ 1, then the error of approximating cos x by 1 − x^2/2 is bounded by (5/96)|x|^4.
Русский
Если |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_bound {x : ℝ} (hx : |x| ≤ 1) : |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96) :=
calc
|cos x - (1 - x ^ 2 / 2)| = ‖Complex.cos x - (1 - (x : ℂ) ^ 2 / 2)‖ := by rw [← Real.norm_eq_abs, ← norm_real]; simp
_ = ‖(Complex.exp (x * I) + Complex.exp (-x * I) - (2 - (x : ℂ) ^ 2)) / 2‖ := by
simp [Complex.cos, sub_div, add_div]
_ =
‖((Complex.exp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / m.factorial) +
(Complex.exp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / m.factorial)) /
2‖ :=
(congr_arg (‖·‖ : ℂ → ℝ)
(congr_arg (fun x : ℂ => x / 2)
(by
simp only [neg_mul, pow_succ, pow_zero, sum_range_succ, range_zero, sum_empty, Nat.factorial, Nat.cast_succ,
zero_add, mul_one, Nat.mul_one, mul_neg, neg_neg]
apply Complex.ext <;> simp [div_eq_mul_inv, normSq] <;> ring_nf)))
_ ≤
‖(Complex.exp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / m.factorial) / 2‖ +
‖(Complex.exp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / m.factorial) / 2‖ :=
by rw [add_div]; exact norm_add_le _ _
_ =
‖Complex.exp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / m.factorial‖ / 2 +
‖Complex.exp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / m.factorial‖ / 2 :=
by simp
_ ≤
‖x * I‖ ^ 4 * (Nat.succ 4 * ((Nat.factorial 4) * (4 : ℕ) : ℝ)⁻¹) / 2 +
‖-x * I‖ ^ 4 * (Nat.succ 4 * ((Nat.factorial 4) * (4 : ℕ) : ℝ)⁻¹) / 2 :=
by
gcongr
· exact Complex.exp_bound (by simpa) (by decide)
· exact Complex.exp_bound (by simpa) (by decide)
_ ≤ |x| ^ 4 * (5 / 96) := by norm_num [Nat.factorial]
