Charlier polynomials

DefinitionUnsigned Charlier polynomials of order 0#✓fully proved

For a semiring \(R\) and a natural number \(n\), the \(n\)-th unsigned Charlier polynomial of order \(0\) is

\[\sum_{k=0}^{n} \binom{n}{k}\, x^{\overline{k}} \in R[x],\]

where \(x^{\overline{k}} = x(x+1)\cdots(x+k-1)\) is the rising factorial polynomial.

It is the terminating hypergeometric series \({}_2F_0(-n, x; ; -1)\), an unsigned version of the Charlier polynomials of order 0, and its coefficient array is the exponential Riordan array \([e^x, \ln(1/(1-x))]\).

noncomputable def unsignedCharlierOrder0 (R : Type*) [Semiring R] (n : ℕ) : Polynomial R :=
  ∑ k ∈ Finset.range (n + 1), (n.choose k) • ascPochhammer R k

Used by 1

Used byCoefficients of the unsigned Charlier polynomials

DefinitionUnsigned Charlier coefficient#✓fully proved

For natural numbers \(n\) and \(m\), the unsigned Charlier coefficient is the natural number

\[c(n, m) = \sum_{k=0}^{n} \binom{n}{k}\, [x^m]\, x^{\overline{k}},\]

where \(x^{\overline{k}} = x(x+1)\cdots(x+k-1)\) is the rising factorial polynomial over \(\mathbb{N}\) and \([x^m]\) denotes the coefficient of \(x^m\).

noncomputable def unsignedCharlierCoeff (n m : ℕ) : ℕ :=
  ∑ k ∈ Finset.range (n + 1), (n.choose k) * (ascPochhammer ℕ k).coeff m

Used by 1

Used byCoefficients of the unsigned Charlier polynomials

TheoremCoefficients of the unsigned Charlier polynomials#✓fully proved

For all natural numbers \(n\) and \(m\), the coefficient of \(x^m\) in the \(n\)-th unsigned Charlier polynomial of order \(0\) over \(\mathbb{N}\) equals the unsigned Charlier coefficient \(c(n, m)\).

theorem unsignedCharlier_coeff_eq (n m : ℕ) :
    (unsignedCharlierOrder0 ℕ n).coeff m = unsignedCharlierCoeff n m

Uses 2

Statement usesUnsigned Charlier coefficient · Unsigned Charlier polynomials of order 0

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.