English
For general affine data (n, x, a1, b1, m, a2, b2) with the given bounds, the bound transfers to the previous step: |e^x − expNear n x a1| ≤ |x|^n/n! · b1.
Русский
При заданных ограничениях переход промежуточной аппроксимации сохраняется в предыдущий шаг: |e^x − expNear n x a1| ≤ |x|^n/n! · b1.
LaTeX
$$$|e^{x} - \\expNear(n, x, a_{1})| \\leq \\frac{|x|^{n}}{n!} \\cdot b_{1}.$$$
Lean4
theorem exp_approx_succ {n} {x a₁ b₁ : ℝ} (m : ℕ) (e₁ : n + 1 = m) (a₂ b₂ : ℝ)
(e : |1 + x / m * a₂ - a₁| ≤ b₁ - |x| / m * b₂) (h : |exp x - expNear m x a₂| ≤ |x| ^ m / m.factorial * b₂) :
|exp x - expNear n x a₁| ≤ |x| ^ n / n.factorial * b₁ :=
by
refine (abs_sub_le _ _ _).trans ((add_le_add_right h _).trans ?_)
subst e₁; rw [expNear_succ, expNear_sub, abs_mul]
convert mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_ using 1
· simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]
ac_rfl
· simp [div_nonneg, abs_nonneg]
