exp_pos — Mathlib

English

Let x ∈ C with |x| ≤ 1 and n > 0. Then the remainder after truncating exp at n terms satisfies an upper bound in terms of |x|.

Русский

Пусть x ∈ C, при этом |x| ≤ 1 и n > 0. Тогда остаток после апроксимации экспоненты суммой до n−го слагаемого удовлетворяет верхней границе в зависимости от |x|.

LaTeX

$$$\|\exp x - \sum_{m=0}^{n-1} \frac{x^m}{m!}\| \le \|x\|^n \cdot ((n+1) / (n!\, n))$$$

Lean4

@[bound]
theorem exp_pos (x : ℝ) : 0 < exp x :=
  (le_total 0 x).elim (lt_of_lt_of_le zero_lt_one ∘ one_le_exp) fun h =>
    by
    rw [← neg_neg x, Real.exp_neg]
    exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

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