Commit 2025-10-28 22:21 4ca9b01d

View on Github →

feat(Analysis/Calculus): Taylor series converges to function on whole ball (#26267)

  • Prove FormalMultilinearSeries.AnalyticOnNhd: the sum of series is analytic on its ball of convergence.
  • Prove AnalyticOn.hasFPowerSeriesOnBall: a variant of AnalyticAt.hasFPowerSeriesAt which gives convergence to the function on the ball of convergence.

Estimated changes