exp_sub_sum_range_succ_isLittleO_pow

English

For every n ∈ ℕ, exp(x) minus the sum up to n of x^i / i! is little-o 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

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