abs_exp_sub_one_le — Mathlib

English

If |x| ≤ 1, then |expNear n x r| ≤ a bound which is linear in r and depends on x; specifically, abs expNear is bounded by a linear expression in r with coefficients depending on x.

Русский

Если |x| ≤ 1, то значение expNear(n, x, r) ограничено линейной функцией от r с коэффициентами зависящими от x.

LaTeX

$$$|\\operatorname{expNear}(n, x, r)| \\leq \\sum_{m=0}^{n-1} \\frac{|x|^{m}}{m!} + |x|^{n} \\frac{|r|}{n!}.$$$

Lean4

theorem abs_exp_sub_one_le {x : ℝ} (hx : |x| ≤ 1) : |exp x - 1| ≤ 2 * |x| :=
  by
  have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
  exact_mod_cast Complex.norm_exp_sub_one_le (x := x) this

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