Taylor series converges to function on whole ball

In this file we prove that if a function f is analytic on the ball of convergence of its Taylor series, then the series converges to f on this ball.

theorem AnalyticOn.hasFPowerSeriesOnSubball {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {r : ENNReal} (hr_pos : 0 < r) (h : AnalyticOn 𝕜 f (EMetric.ball x r)) : r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial).radius → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial) x r

If f is analytic on Bᵣ(x₀) and its Taylor series converges on this ball, then it converges to f.

theorem AnalyticOn.hasFPowerSeriesOnBall {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} : 0 < (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial).radius → AnalyticOn 𝕜 f (EMetric.ball x (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial).radius) → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial) x (FormalMultilinearSeries.ofScalars 𝕜 fun (n : ℕ) => iteratedDeriv n f x / ↑n.factorial).radius

If f is analytic on the ball of convergence of its Taylor series, then the series converges to f on this ball. This is a stronger version of AnalyticAt.hasFPowerSeriesAt that requires the assumption RCLike 𝕜.

For example, over the p-adic numbers, the indicator function of the unit ball is analytic everywhere, but it agrees with the sum of its Taylor series only on this unit ball.