exp_approx_start — Mathlib

English

Exp bound at the start of the series provides a coarse control of the exponential by the first few terms.

Русский

Начальное ограничение экспоненты обеспечивает грубый контроль экспоненты через первые члены ряда.

LaTeX

$$$|e^{x} - \\sum_{m=0}^{0} \\frac{x^{m}}{m!}| \\leq \\cdots$$$

Lean4

theorem exp_approx_start (x a b : ℝ) (h : |exp x - expNear 0 x a| ≤ |x| ^ 0 / Nat.factorial 0 * b) : |exp x - a| ≤ b :=
  by simpa using h

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