expSeries_summable'

Mathlib.Analysis.Normed.Algebra.Exponential

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

English

The HasSum for the inverse-weighted exponential series equals exp(x): HasSum n!^{-1} x^n = exp(x).

Русский

Сумма с весами n!^{-1} x^n равна exp(x).

LaTeX

$$$\text{HasSum } \left( (n !^{-1}) \cdot x^n \right) = \exp 𝕂 x$$$

Lean4

theorem expSeries_summable' (x : 𝔸) : Summable fun n => (n !⁻¹ : 𝕂) • x ^ n :=
  (norm_expSeries_summable' x).of_norm

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

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

Разделы

Аффилиация

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