norm_expSeries_summable' — Mathlib

English

Has summable sequence of norms with factorial inverse weights: Summable n ↦ ∥(n!^{-1}) • x^n∥.

Русский

Суммируемость последовательности норм с весами, умноженными на (n!)^{-1}: сумма ∥(n!)^{-1} • x^n∥ сходится.

LaTeX

$$$\text{Summable } \Big(\| (n !^{-1}) \cdot x^n \|\Big)$$$

Lean4

theorem norm_expSeries_summable' (x : 𝔸) : Summable fun n => ‖(n !⁻¹ : 𝕂) • x ^ n‖ :=
  norm_expSeries_summable_of_mem_ball' x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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