abs_exp_sub_one_sub_id_le — Mathlib

English

ExpNear is affine in its tail parameter: expNear(n, x, r1) − expNear(n, x, r2) = x^n/n! · (r1 − r2).

Русский

ExpNear по переменной r линейна: expNear(n, x, r1) − expNear(n, x, r2) = x^n/n! · (r1 − r2).

LaTeX

$$$\\operatorname{expNear}(n, x, r_{1}) - \\operatorname{expNear}(n, x, r_{2}) = \\frac{x^{n}}{n!} (r_{1} - r_{2}).$$$

Lean4

theorem abs_exp_sub_one_sub_id_le {x : ℝ} (hx : |x| ≤ 1) : |exp x - 1 - x| ≤ x ^ 2 :=
  by
  rw [← sq_abs]
  have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
  exact_mod_cast Complex.norm_exp_sub_one_sub_id_le this

Похожие утверждения