norm_expSeries_div_summable — Mathlib

English

The series of norms of x^n / n! is summable: ∑ ‖x^n / n!‖ converges.

Русский

Ряд норм сумм экспонентной части ∑ ‖x^n / n!‖ сходится.

LaTeX

$$$\\sum_{n=0}^{\\infty} \\left\\| \\frac{x^{n}}{n!} \\right\\| < \\infty$$$

Lean4

theorem norm_expSeries_div_summable (x : 𝔸) : Summable fun n => ‖(x ^ n / n ! : 𝔸)‖ :=
  norm_expSeries_div_summable_of_mem_ball 𝕂 x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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