expSeries_summable

Mathlib.Analysis.Normed.Algebra.Exponential

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

English

The exponential series is summable: sum of expSeries terms converges to exp.

Русский

Ряд экспоненты суммируем: сумма членов expSeries сходится к exp.

LaTeX

$$$\text{Summable } \big( \expSeries 𝕂 𝔸 n (\,\cdot\, x) \big)$$$

Lean4

theorem expSeries_summable (x : 𝔸) : Summable fun n => expSeries 𝕂 𝔸 n fun _ => x :=
  (norm_expSeries_summable x).of_norm

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

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

Разделы

Аффилиация

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