Commit 2025-11-06 19:26 9397b2fc

View on Github →

feat(Analysis): binomial series convergence (#31047) Prove

one_add_cpow_hasFPowerSeriesOnBall_zero: for complex a and |x| < 1, the binomial series converges to (1 + x).cpow a.
one_add_rpow_hasFPowerSeriesOnBall_zero: the variant of the above for reals.

Estimated changes

Modified Mathlib/Analysis/Analytic/Binomial.lean

added theorem Complex.ofReal_choose

added theorem binomialSeries_apply

added theorem binomialSeries_radius_ge_one

added theorem one_add_cpow_hasFPowerSeriesAt_zero

added theorem one_add_cpow_hasFPowerSeriesOnBall_zero

added theorem one_add_rpow_hasFPowerSeriesAt_zero

added theorem one_add_rpow_hasFPowerSeriesOnBall_zero

Modified Mathlib/RingTheory/Binomial.lean

added theorem Ring.map_choose

added theorem Ring.map_multichoose