exp_bound — Mathlib

English

If |x| ≤ 1, then for any n > 0, |e^x − ∑_{m=0}^{n-1} x^m/m!| ≤ |x|^n · (n+1)/(n! · n).

Русский

Если |x| ≤ 1, то при любом n > 0 выполняется неравенство аналогичное: |e^x − частичная сумма| ≤ |x|^n · (n+1)/(n! · n).

LaTeX

$$$\\left|e^{x} - \\sum_{m=0}^{n-1} \\frac{x^{m}}{m!}\\right| \\leq |x|^{n} \\cdot \\frac{n+1}{n! \\; n}.$$

Lean4

nonrec theorem exp_bound {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) :
    |exp x - ∑ m ∈ range n, x ^ m / m.factorial| ≤ |x| ^ n * (n.succ / (n.factorial * n)) :=
  by
  have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
  convert exp_bound hxc hn using 2 <;> norm_cast

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