expSeries_div_summable_of_mem_ball

English

The exponential series x^n / n! is summable (termwise) for x in the radius of convergence.

Русский

Ряд экспоненты x^n / n! суммируем в радиусе конвергенции.

LaTeX

$$$\text{Summable } \left( x^n / n! \right) \quad \text{for } x \in B(0, \operatorname{radius}(\expSeries 𝕂 𝔸))$$$

Lean4

theorem expSeries_div_summable_of_mem_ball [CompleteSpace 𝔸] (x : 𝔸)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : Summable fun n => x ^ n / n ! :=
  (norm_expSeries_div_summable_of_mem_ball 𝕂 x hx).of_norm

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