Theorems · Theorem · special functions

Complex.regularizedHGFunCoeff_add_one

∀ {a b : Multiset ℂ} {n : ℕ},
  (∀ k ∈ b, k ≠ -↑n) →
    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: 1 results in Mathlib
Foundations: Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Complexstatement and proof · cited by 5,565
Multisetstatement and proof · cited by 2,627
Nat.cast_oneproof · cited by 2,501
Multiset.mapstatement and proof · cited by 876
Polynomial.evalproof · cited by 796
Nat.factorialproof · cited by 616
Nat.cast_addproof · cited by 586
Multiset.prodstatement and proof · cited by 528
Multiset.map_congrproof · cited by 232
Polynomial.eval_Xproof · cited by 172
Polynomial.eval_mulproof · cited by 127
Complex.Gammaproof · cited by 96

Cited by1

Results whose statement or proof uses this declaration.

Complex.regularizedHGFunCoeff_add_one_div_selfproof · cited by 2