Commit 2025-12-10 16:38 ed8f8ad4

View on Github →

feat(Analysis): HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x)) and friends (#32373)

Estimated changes

Modified Mathlib/Analysis/Analytic/Binomial.lean

added theorem Complex.hasFPowerSeriesOnBall_ofScalars_mul_add_zero

added theorem Complex.one_add_cpow_hasFPowerSeriesAt_zero

added theorem Complex.one_add_cpow_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_sub_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero

added theorem Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero

added theorem Real.hasFPowerSeriesOnBall_linear_zero

added theorem Real.one_add_rpow_hasFPowerSeriesAt_zero

added theorem Real.one_add_rpow_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_one_sub_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_sub_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero

added theorem Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero

deleted theorem one_add_cpow_hasFPowerSeriesAt_zero

deleted theorem one_add_cpow_hasFPowerSeriesOnBall_zero

deleted theorem one_add_rpow_hasFPowerSeriesAt_zero

deleted theorem one_add_rpow_hasFPowerSeriesOnBall_zero

Modified Mathlib/Analysis/Analytic/OfScalars.lean

added theorem FormalMultilinearSeries.ofScalars_sub