norm_expSeries_summable — Mathlib

English

For x in ball, the sequence of norms of expSeries terms is summable: Summable n ↦ ∥expSeries 𝕂 𝔸 n fun _ => x∥.

Русский

Для x внутри шара последовательность норм экспоненциальных коэффициентов суммируема: сумма по нормам ∥expSeries n∥ прерывно сходится.

LaTeX

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

Lean4

theorem norm_expSeries_summable (x : 𝔸) : Summable fun n => ‖expSeries 𝕂 𝔸 n fun _ => x‖ :=
  norm_expSeries_summable_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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