summable_powerSeries_of_norm_lt_one

English

If a power series converges at 1, it converges absolutely for all z with ∥z∥ < 1.

Русский

Если степенной ряд сходится в точке 1, то он сходится по модулю в любой точке с нормой меньше 1.

LaTeX

$$$\forall {f : \mathbb{N} \to E} [\text{NormedDivisionRing } E] {z : E} (h : CauchySeq (n \mapsto \sum_{i< n} f(i) z^i)) (hz : \|z\| < 1) \\ → \\ Summable (n \mapsto f(n) z^n)$$$

Lean4

/-- If a power series converges at 1, it converges absolutely at all `z` of smaller norm. -/
theorem summable_powerSeries_of_norm_lt_one {z : α} (h : CauchySeq fun n ↦ ∑ i ∈ range n, f i) (hz : ‖z‖ < 1) :
    Summable fun n ↦ f n * z ^ n :=
  summable_powerSeries_of_norm_lt (w := 1) (by simp [h]) (by simp [hz])

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