Binomial series for the ascending Pochhammer symbol

The generating function (\sum_n (a)_n t^n / n! = (1-t)^{-a}) for (|t| < 1), written in Mathlib's ascPochhammer and Ring.multichoose language.

theorem Complex.ascPochhammer_eval_div_factorial (a : ℂ) (n : ℕ) : Polynomial.eval a (ascPochhammer ℂ n) / ↑n.factorial = Ring.multichoose a n

Ascending Pochhammer symbols divided by factorials are the binomial-ring multichoose coefficients.

theorem Complex.hasSum_ascPochhammer_mul_pow_div_factorial (a t : ℂ) (ht : ‖t‖ < 1) : HasSum (fun (n : ℕ) => Polynomial.eval a (ascPochhammer ℂ n) / ↑n.factorial * t ^ n) (1 / (1 - t) ^ a)

The binomial series (\sum (a)_n t^n / n! = (1-t)^{-a}) inside the unit disk.

theorem Complex.summable_norm_ascPochhammer_mul_pow_div_factorial (a t : ℂ) (ht : ‖t‖ < 1) : Summable fun (n : ℕ) => ‖Polynomial.eval a (ascPochhammer ℂ n) / ↑n.factorial * t ^ n‖

The binomial series of hasSum_ascPochhammer_mul_pow_div_factorial is absolutely summable inside the unit disk.