exp_approx_end — Mathlib

English

If n+1 = m and |x| ≤ 1, then |e^x − expNear m x 0| ≤ |x|^m/m! · ((m+1)/m).

Русский

Если n+1 = m и |x| ≤ 1, то |e^x − expNear(m, x, 0)| ≤ |x|^m/m! · ((m+1)/m).

LaTeX

$$$\\left|e^{x} - \\expNear(m, x, 0)\\right| \\leq \\frac{|x|^{m}}{m!} \\cdot \\frac{m+1}{m}. $$$

Lean4

theorem exp_approx_end (n m : ℕ) (x : ℝ) (e₁ : n + 1 = m) (h : |x| ≤ 1) :
    |exp x - expNear m x 0| ≤ |x| ^ m / m.factorial * ((m + 1) / m) :=
  by
  simp only [expNear, mul_zero, add_zero]
  convert exp_bound (n := m) h ?_ using 1
  · simp [field]
  · cutsat

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