Theorems · Theorem · special functions

Complex.coeff_regularizedGaussHGFunSeries

∀ {n : ℕ} {a b c : ℂ},
  (a.regularizedGaussHGFunSeries b c).coeff n =
    Polynomial.eval a (ascPochhammer ℂ n) * Polynomial.eval b (ascPochhammer ℂ n) /
      (↑n.factorial * Complex.Gamma (c + ↑n))

Defined in: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Cited by: 1 results in Mathlib
Foundations: Depth 257 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.

Cites12

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
Polynomial.evalstatement and proof · cited by 796
Nat.factorialstatement and proof · cited by 616
Multiset.prodproof · cited by 528
Complex.Gammastatement and proof · cited by 96
Multiset.map_consproof · cited by 93
ascPochhammerstatement and proof · cited by 80
Multiset.prod_consproof · cited by 68
FormalMultilinearSeries.coeffstatement · cited by 30
Multiset.prod_singletonproof · cited by 29
Complex.regularizedGaussHGFunSeriesstatement · cited by 9
Complex.regularizedHGFunSeries_coeffproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

Complex.Gamma_inv_mul_ordinaryHypergeometricSeries_eqproof · cited by 1