exp_sub_sum_range_succ_isLittleO_pow

English

For each n ∈ ℕ, exp x minus ∑_{i=0}^{n} x^i / i! is little-oh of |x|^n as x → 0.

Русский

Для каждого n ∈ ℕ exp x минус сумма до n включительно x^i / i! является little-o по отношению к |x|^n при x → 0.

LaTeX

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

Lean4

theorem exp_sub_sum_range_succ_isLittleO_pow (n : ℕ) :
    (fun x ↦ exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / i !) =o[𝓝 0] (· ^ n) :=
  (exp_sub_sum_range_isBigO_pow (n + 1)).trans_isLittleO <| isLittleO_pow_pow n.lt_succ_self

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