lean_workbook_plus_1011
ProvedLet be a power series ( ). Suppose that converges at where . Show that converges at any with .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1011 (a : ℕ → ℝ) (c x : ℝ) (hc : 0 < c) (hx : |x| < c) : ∃ y : ℝ, y = ∑' k : ℕ, a k * x ^ k := by sorry
Source