English
If |x| ≤ 1, then the error of approximating sin x by x − x^3/6 is bounded by (5/96)|x|^4.
Русский
Если |x| ≤ 1, то погрешность аппроксимации sin x через x − x^3/6 не превышает (5/96)|x|^4.
LaTeX
$$$\\\\forall x \\\\in \\\\mathbb{R}, |x| \\\\le 1 \\\\Rightarrow \\\\left| \\\\sin x - \\left(x - \\\\frac{x^3}{6}\\\\right) \\\\right| \\\\le |x|^4 \\\\left(\\\\frac{5}{96}\\\\right)$$$
Lean4
theorem sin_bound {x : ℝ} (hx : |x| ≤ 1) : |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96) :=
calc
|sin x - (x - x ^ 3 / 6)| = ‖Complex.sin x - (x - x ^ 3 / 6 : ℝ)‖ := by rw [← Real.norm_eq_abs, ← norm_real]; simp
_ = ‖((Complex.exp (-x * I) - Complex.exp (x * I)) * I - (2 * x - x ^ 3 / 3 : ℝ)) / 2‖ := by
simp [Complex.sin, sub_div, mul_div_cancel_left₀ _ (two_ne_zero' ℂ), div_div, show (3 : ℂ) * 2 = 6 by norm_num]
_ =
‖((Complex.exp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / m.factorial) -
(Complex.exp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / m.factorial)) *
I /
2‖ :=
(congr_arg (‖·‖ : ℂ → ℝ)
(congr_arg (fun x : ℂ => x / 2)
(by
simp only [neg_mul, pow_succ, pow_zero, ofReal_sub, ofReal_mul, ofReal_ofNat, ofReal_div, sum_range_succ,
range_zero, sum_empty, Nat.factorial, Nat.cast_succ, zero_add, mul_neg, mul_one, neg_neg, Nat.mul_one]
apply Complex.ext <;> simp [div_eq_mul_inv, normSq]; ring)))
_ ≤
‖(Complex.exp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / m.factorial) * I / 2‖ +
‖-((Complex.exp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / m.factorial) * I) / 2‖ :=
by rw [sub_mul, sub_eq_add_neg, 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 [add_comm]
_ ≤
‖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]
