exp_sub_sum_range_isBigO_pow — Mathlib

English

For every n ∈ ℕ, exp(x) minus its nth Taylor polynomial at 0 is of order O(|x|^n) as x → 0.

Русский

Для каждого натурального n остаток ряда exp(x) после полинома Тейлора степени n вокруг 0 имеет порядок O(|x|^n) при x → 0.

LaTeX

$$$$ \\exp x - \\sum_{i=0}^{n-1} \\frac{x^i}{i!} = O(|x|^n) \\quad \\text{as } x \\to 0. $$$$

Lean4

theorem exp_sub_sum_range_isBigO_pow (n : ℕ) : (fun x ↦ exp x - ∑ i ∈ Finset.range n, x ^ i / i !) =O[𝓝 0] (· ^ n) :=
  by
  rcases (zero_le n).eq_or_lt with rfl | hn
  · simpa using continuous_exp.continuousAt.norm.isBoundedUnder_le
  · refine .of_bound (n.succ / (n ! * n)) ?_
    rw [NormedAddCommGroup.nhds_zero_basis_norm_lt.eventually_iff]
    refine ⟨1, one_pos, fun x hx ↦ ?_⟩
    convert exp_bound hx.out.le hn using 1
    simp [field]

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