Convergence of multichoose power series

This file determines the exact unconditional summability domain of the power series with generalized multichoose coefficients and positive real parameter. The result applies to both real and complex arguments. These results supply the analytic criterion used to determine the exact integrability domain of the negative-binomial probability-generating function.

Main declarations

• TauCeti.hasSum_multichoose_mul_geometric_of_abs_lt_one — the multichoose binomial series on the open unit interval.
• TauCeti.hasSum_multichoose_mul_geometric_complex_of_norm_lt_one — the complex-valued multichoose binomial series on the open unit disk.
• TauCeti.summable_multichoose_mul_geometric_iff_norm_lt_one — exact summability of ∑ n, multichoose r n * q ^ n for 0 < r.

theorem TauCeti.hasSum_multichoose_mul_geometric_of_abs_lt_one {r x : ℝ} (hx : |x| < 1) : HasSum (fun (n : ℕ) => Ring.multichoose r n * x ^ n) (1 / (1 - x) ^ r)

The generalized multichoose power series sums to (1 - x)⁻ʳ when |x| < 1.

theorem TauCeti.hasSum_multichoose_mul_geometric_complex_of_norm_lt_one {r z : ℂ} (hz : ‖z‖ < 1) : HasSum (fun (n : ℕ) => Ring.multichoose r n * z ^ n) (1 / (1 - z) ^ r)

The generalized multichoose power series sums to (1 - z)⁻ʳ throughout the complex open unit disk.

@[simp]

theorem TauCeti.summable_multichoose_mul_geometric_iff_norm_lt_one {𝕂 : Type u_1} [RCLike 𝕂] {r : ℝ} {q : 𝕂} (hr : 0 < r) : (Summable fun (n : ℕ) => ↑(Ring.multichoose r n) * q ^ n) ↔ ‖q‖ < 1

For positive real r, the generalized multichoose power series is unconditionally summable at a real or complex argument q exactly when q lies in the open unit ball.