Commit 2024-12-18 06:37 2144977f

feat(Analysis/Analytic): FormalMultilinearSeries.unshift convergence (#19848)

• Prove unshift_shift, which states that p.unshift.shift = p.
• Prove radius_shift and radius_unshift, which state that the shifted and unshifted series converge on the same ball.
• Prove HasFPowerSeriesOnBall.unshift (and variations), describing where the shifted series converges.