Theorems · Theorem · special functions

Complex.regularizedHGFunCoeff_add_one_div_self

∀ {a b : Multiset ℂ} {n : ℕ},
  Complex.regularizedHGFunCoeff a b n ≠ 0 →
    Complex.regularizedHGFunCoeff a b (n + 1) / Complex.regularizedHGFunCoeff a b n =
      (Multiset.map (fun x => x + ↑n) a).prod / ((Multiset.map (fun x => x + ↑n) b).prod * (↑n + 1))

Recursion formula for the coefficients of the hypergeometric series. This is mainly used to calculate the convergence radius.

Defined in

Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Cited by

2 results in Mathlib

Foundations

Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound