Existence_of_Interval_of_Convergence_of_Power_Series
Provedpower-seriesproofwikiseries
Every power series has a radius of convergence R >= 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Existence_of_Interval_of_Convergence_of_Power_Series (a : ℕ → ℝ) : ∃ R : ℝ, 0 ≤ R ∧ (∀ x : ℝ, |x| < R → Summable (fun n => a n * x ^ n)) := by sorry
Source