norm_expSeries_div_summable_of_mem_ball

English

For x in the ball, the sequence of norms of the terms x^n / n! is summable: the norm series converges.

Русский

Для x внутри шара последовательность норм членов x^n / n! сходится: ряд норм сходится.

LaTeX

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

Lean4

theorem norm_expSeries_div_summable_of_mem_ball (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    Summable fun n => ‖x ^ n / (n ! : 𝔸)‖ := by
  change Summable (norm ∘ _)
  rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]
  exact norm_expSeries_summable_of_mem_ball x hx

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