English
If a power series converges at w, then it converges absolutely at all z with ∥z∥ < ∥w∥.
Русский
Если степенной ряд сходится в точке w, то он сходится по модулю и в любой точке z с меньшей нормой, чем ∥w∥.
LaTeX
$$$\forall {f : \mathbb{N} \to E} [\text{NormedDivisionRing } E] {w z : E} (h : CauchySeq (n \mapsto \sum_{i< n} f(i) w^i)) (hz : \|z\| < \|w\|) \\ → \\ Summable (n \mapsto f(n) z^n)$$$
Lean4
/-- If a power series converges at `w`, it converges absolutely at all `z` of smaller norm. -/
theorem summable_powerSeries_of_norm_lt {w z : α} (h : CauchySeq fun n ↦ ∑ i ∈ range n, f i * w ^ i) (hz : ‖z‖ < ‖w‖) :
Summable fun n ↦ f n * z ^ n :=
by
have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz
obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h
rw [summable_iff_cauchySeq_finset]
refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz) (fun n ↦ ?_)
rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]
conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]
exact mul_le_mul_of_nonneg_right (hC n) (pow_nonneg (norm_nonneg z) n)
