Jacobi–Stirling and Legendre–Stirling numbers

DefinitionGenerating polynomial of the first-kind Jacobi–Stirling numbers#✓fully proved

For a commutative ring \(R\), an element \(\zeta \in R\) and a natural number \(n\), the \(n\)-th first-kind Jacobi–Stirling generating polynomial is \(\prod_{i=0}^{n-1} (X - i(i + \zeta))\) in \(R[X]\).

public noncomputable def jacobiStirlingFirstPoly {R : Type*} [CommRing R]
    (n : ℕ) (ζ : R) : Polynomial R :=
  ∏ i ∈ Finset.range n,
    (Polynomial.X - Polynomial.C ((i : R) * ((i : R) + ζ)))

Used by 4

Used byFirst-kind Jacobi–Stirling numbers · Initial row of the first-kind Jacobi–Stirling numbers · Recurrence for the first-kind Jacobi–Stirling numbers · Generating polynomial of the Legendre–Stirling numbers of the first kind

DefinitionFirst-kind Jacobi–Stirling numbers#✓fully proved

For a commutative ring \(R\), an element \(\zeta \in R\) and natural numbers \(n\) and \(k\), the first-kind Jacobi–Stirling number \(J(n,k;\zeta)\) is the coefficient of \(X^k\) in the polynomial \(\prod_{i=0}^{n-1} (X - i(i + \zeta))\) over \(R\).

public noncomputable def jacobiStirlingFirst {R : Type*} [CommRing R]
    (n k : ℕ) (ζ : R) : R :=
  (jacobiStirlingFirstPoly n ζ).coeff k

Uses 1 · Used by 7

Statement usesGenerating polynomial of the first-kind Jacobi–Stirling numbers

Used byInversion formula for the arrays \(u(k, m)\) and \(U(k, m)\) (Butzer et al.) · Diagonal of the first-kind Jacobi–Stirling numbers · Initial row of the first-kind Jacobi–Stirling numbers · Recurrence for the first-kind Jacobi–Stirling numbers · First-kind Jacobi–Stirling numbers vanish above the diagonal · Legendre–Stirling numbers of the first kind · Recurrence for the Legendre–Stirling numbers of the first kind

TheoremInitial row of the first-kind Jacobi–Stirling numbers#✓fully proved

For every commutative ring \(R\), every \(\zeta \in R\) and every natural number \(k\), the first-kind Jacobi–Stirling number \(J(0,k;\zeta)\) equals \(1\) if \(k = 0\) and \(0\) otherwise.

public theorem jacobiStirlingFirst_initial_row {R : Type*} [CommRing R]
    (k : ℕ) (ζ : R) :
    jacobiStirlingFirst 0 k ζ = if k = 0 then 1 else 0

Uses 2 · Used by 3

Statement usesFirst-kind Jacobi–Stirling numbers

Proof usesGenerating polynomial of the first-kind Jacobi–Stirling numbers

Used byDiagonal of the first-kind Jacobi–Stirling numbers · First-kind Jacobi–Stirling numbers vanish above the diagonal · Initial row of the Legendre–Stirling numbers of the first kind

TheoremRecurrence for the first-kind Jacobi–Stirling numbers#✓fully proved

For every commutative ring \(R\), every \(\zeta \in R\) and all natural numbers \(n\) and \(k\), the first-kind Jacobi–Stirling numbers satisfy \(J(n+1,k+1;\zeta) = J(n,k;\zeta) - n(n + \zeta)\,J(n,k+1;\zeta)\).

public theorem jacobiStirlingFirst_recurrence {R : Type*} [CommRing R]
    (n k : ℕ) (ζ : R) :
    jacobiStirlingFirst (n + 1) (k + 1) ζ =
      jacobiStirlingFirst n k ζ -
        (n : R) * ((n : R) + ζ) * jacobiStirlingFirst n (k + 1) ζ

Uses 2 · Used by 3

Statement usesFirst-kind Jacobi–Stirling numbers

Proof usesGenerating polynomial of the first-kind Jacobi–Stirling numbers

Used byDiagonal of the first-kind Jacobi–Stirling numbers · First-kind Jacobi–Stirling numbers vanish above the diagonal · Recurrence for the Legendre–Stirling numbers of the first kind

TheoremFirst-kind Jacobi–Stirling numbers vanish above the diagonal#✓fully proved

For every commutative ring \(R\), every \(\zeta \in R\) and all natural numbers \(n < k\), the first-kind Jacobi–Stirling number \(J(n,k;\zeta)\) equals \(0\).

public theorem jacobiStirlingFirst_support {R : Type*} [CommRing R]
    (n k : ℕ) (ζ : R) (h : n < k) :
    jacobiStirlingFirst n k ζ = 0

Uses 3 · Used by 2

Statement usesFirst-kind Jacobi–Stirling numbers

Proof usesInitial row of the first-kind Jacobi–Stirling numbers · Recurrence for the first-kind Jacobi–Stirling numbers

Used byDiagonal of the first-kind Jacobi–Stirling numbers · Legendre–Stirling numbers of the first kind vanish above the diagonal

TheoremDiagonal of the first-kind Jacobi–Stirling numbers#✓fully proved

For every commutative ring \(R\), every \(\zeta \in R\) and every natural number \(n\), the first-kind Jacobi–Stirling number \(J(n,n;\zeta)\) equals \(1\).

public theorem jacobiStirlingFirst_diagonal {R : Type*} [CommRing R]
    (n : ℕ) (ζ : R) :
    jacobiStirlingFirst n n ζ = 1

Uses 4 · Used by 1

Statement usesFirst-kind Jacobi–Stirling numbers

Proof usesInitial row of the first-kind Jacobi–Stirling numbers · Recurrence for the first-kind Jacobi–Stirling numbers · First-kind Jacobi–Stirling numbers vanish above the diagonal

Used byDiagonal Legendre–Stirling numbers of the first kind

DefinitionGenerating polynomial of the Legendre–Stirling numbers of the first kind#✓fully proved

For a natural number \(n\), this is the polynomial \(\prod_{i=0}^{n-1} \bigl(X - i(i+1)\bigr)\) with integer coefficients; for \(n = 0\) it is the empty product \(1\).

noncomputable def legendreStirlingFirstPoly (n : ℕ) : Polynomial ℤ :=
  jacobiStirlingFirstPoly n (1 : ℤ)

Uses 1

Statement usesGenerating polynomial of the first-kind Jacobi–Stirling numbers

DefinitionLegendre–Stirling numbers of the first kind#✓fully proved

For natural numbers \(n\) and \(k\), the Legendre–Stirling number of the first kind \(J(n, k; 1)\) is the coefficient of \(x^k\) in the integer polynomial \(\prod_{i=0}^{n-1} \bigl(x - i(i+1)\bigr)\), which is \(1\) when \(n = 0\). These are the Jacobi–Stirling numbers of the first kind \(J(n, k; \zeta)\) at \(\zeta = 1\).

noncomputable def legendreStirlingFirst (n k : ℕ) : ℤ :=
  jacobiStirlingFirst n k (1 : ℤ)

Uses 1 · Used by 6

Statement usesFirst-kind Jacobi–Stirling numbers

Used byThe Faulhaber coefficients \(b_{k,r}\) · The Faulhaber coefficients \(c_{k,r}\) · Diagonal Legendre–Stirling numbers of the first kind · Legendre–Stirling numbers of the first kind vanish above the diagonal · Recurrence for the Legendre–Stirling numbers of the first kind · Initial row of the Legendre–Stirling numbers of the first kind

TheoremInitial row of the Legendre–Stirling numbers of the first kind#✓fully proved

For every natural number \(k\), the Legendre–Stirling number of the first kind \(J(0, k; 1)\) equals \(1\) if \(k = 0\) and \(0\) otherwise.

theorem legendreStirlingFirst_zero (k : ℕ) :
    legendreStirlingFirst 0 k = if k = 0 then 1 else 0

Uses 2

Statement usesLegendre–Stirling numbers of the first kind

Proof usesInitial row of the first-kind Jacobi–Stirling numbers

TheoremRecurrence for the Legendre–Stirling numbers of the first kind#✓fully proved

For all natural numbers \(n\) and \(k\), the Legendre–Stirling numbers of the first kind satisfy \(J(n + 1, k + 1; 1) = J(n, k; 1) - n(n + 1) \, J(n, k + 1; 1)\).

theorem legendreStirlingFirst_succ (n k : ℕ) :
    legendreStirlingFirst (n + 1) (k + 1) =
      legendreStirlingFirst n k -
        (n : ℤ) * ((n + 1 : ℕ) : ℤ) * legendreStirlingFirst n (k + 1)

Uses 3

Statement usesLegendre–Stirling numbers of the first kind

Proof usesFirst-kind Jacobi–Stirling numbers · Recurrence for the first-kind Jacobi–Stirling numbers

TheoremLegendre–Stirling numbers of the first kind vanish above the diagonal#✓fully proved

For all natural numbers \(n < k\), the Legendre–Stirling number of the first kind \(J(n, k; 1)\) is \(0\).

theorem legendreStirlingFirst_eq_zero_of_lt :
    ∀ (n k : ℕ), n < k → legendreStirlingFirst n k = 0

Uses 2

Statement usesLegendre–Stirling numbers of the first kind

Proof usesFirst-kind Jacobi–Stirling numbers vanish above the diagonal

TheoremDiagonal Legendre–Stirling numbers of the first kind#✓fully proved

For every natural number \(n\), the Legendre–Stirling number of the first kind \(J(n, n; 1)\) equals \(1\).

theorem legendreStirlingFirst_diag : ∀ (n : ℕ), legendreStirlingFirst n n = 1

Uses 2

Statement usesLegendre–Stirling numbers of the first kind

Proof usesDiagonal of the first-kind Jacobi–Stirling numbers

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.