expSeries_div_summable

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.expSeries_div_summable

English

The normed version sums: ∑ ‖x^n / n!‖ converges.

Русский

Нормированная версия сходится: ∑ ‖x^n / n!‖ сходится.

LaTeX

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

Lean4

theorem expSeries_div_summable (x : 𝔸) : Summable fun n => x ^ n / n ! :=
  (norm_expSeries_div_summable 𝕂 x).of_norm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru