α-Stirling matrices

DefinitionEntries of the α-Stirling matrix#✓fully proved

Let \(R\) be a commutative ring and let \(\alpha_0, \alpha_1, \alpha_2, \dots\) be a sequence in \(R\) (\(\alpha_0\) is never used). The α-Stirling entries \(s_{i,j} \in R\), for \(i, j \ge 0\), are defined recursively by \(s_{i,0} = \alpha_1\) for all \(i\), \(s_{0,j} = 0\) for \(j \ge 1\), and \(s_{i+1,j+1} = s_{i,j} + \alpha_{j+2} s_{i,j+1}\) for all \(i, j \ge 0\).

These are the entries of the paper's matrix \(S_\alpha(n)\) with indices shifted to start at \(0\). Writing \(\hat S_{i,j}\) for the entries of \(S_\alpha(n)\) in the paper's \(1\)-based indexing, the first column is \(\alpha_1\), the rest of the first row is \(0\), and \(\hat S_{i,j} = \hat S_{i-1,j-1} + \alpha_j \hat S_{i-1,j}\) for \(i, j \ge 2\).

def alphaStirlingEntry (α : ℕ → R) : ℕ → ℕ → R
  | _, 0 => α 1
  | 0, _ + 1 => 0
  | i + 1, j + 1 => alphaStirlingEntry α i j + α (j + 2) * alphaStirlingEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4, equation (a-1).

Used by 3

Used byRecurrence for the α-Stirling entries · First column of the α-Stirling entries · The α-Stirling matrix

DefinitionEntries of the shifted α-Stirling matrix#✓fully proved

Let \(R\) be a commutative ring and let \(\alpha = (\alpha_j)_{j \ge 1}\) be a sequence in \(R\). The entries \(\mathsf{S}_{i,j} \in R\) of the shifted \(\alpha\)-Stirling matrix of \(\alpha\), for natural numbers \(i\) and \(j\) counted from \(0\), are defined by \(\mathsf{S}_{i,0} = \alpha_1\) for all \(i\), \(\mathsf{S}_{0,j} = \alpha_1\) for all \(j\), and

\[\mathsf{S}_{i+1,j+1} = \mathsf{S}_{i+1,j} + \alpha_{j+2} \mathsf{S}_{i,j+1}.\]

The paper indexes from \(1\): its entry \((i, j)\) is \(P_{i,j} = \mathsf{S}_{i-1,j-1}\) for \(i, j \ge 1\). In this indexing the first row and the first column equal \(\alpha_1\), and \(P_{i,j} = P_{i,j-1} + \alpha_j P_{i-1,j}\) for \(i, j \ge 2\).

def shiftedAlphaStirlingEntry (α : ℕ → R) : ℕ → ℕ → R
  | _, 0 => α 1
  | 0, _ + 1 => α 1
  | i + 1, j + 1 =>
      shiftedAlphaStirlingEntry α (i + 1) j + α (j + 2) * shiftedAlphaStirlingEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4.

Used by 3

Used byRecurrence for the shifted α-Stirling entries · First row of the shifted α-Stirling matrix · Shifted α-Stirling matrix

DefinitionEntries of the α-upper matrix#✓fully proved

Let \(R\) be a commutative ring and let \(\alpha_0, \alpha_1, \alpha_2, \dots\) be a sequence in \(R\) (\(\alpha_0\) is never used). The α-upper entries \(u_{i,j} \in R\), for \(i, j \ge 0\), are defined recursively by \(u_{0,j} = 1\) for all \(j\), \(u_{i,0} = 0\) for \(i \ge 1\), and \(u_{i+1,j+1} = u_{i+1,j} + \alpha_{i+1} u_{i,j} + (\alpha_{j+2} - \alpha_{i+1}) u_{i,j+1}\) for all \(i, j \ge 0\).

These are the entries of the paper's matrix \(\mathsf{U}_\alpha(n)\) with indices shifted to start at \(0\); in the paper's \(1\)-based indexing the first row is \(1\), the rest of the first column is \(0\), and \(\mathsf{U}_{i,j} = \mathsf{U}_{i,j-1} + \alpha_{i-1} \mathsf{U}_{i-1,j-1} + (\alpha_j - \alpha_{i-1}) \mathsf{U}_{i-1,j}\) for \(i, j \ge 2\).

def alphaUpperEntry (α : ℕ → R) : ℕ → ℕ → R
  | 0, _ => 1
  | _ + 1, 0 => 0
  | i + 1, j + 1 =>
      alphaUpperEntry α (i + 1) j + α (i + 1) * alphaUpperEntry α i j +
        (α (j + 2) - α (i + 1)) * alphaUpperEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 2, equation (u-1-2).

Used by 4

Used byα-upper entries are complete homogeneous symmetric polynomials · Small α-upper entries · Recurrence for the α-upper entries · The α-upper matrix

TheoremRecurrence for the α-Stirling entries#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(s_{i,j}\) (\(i, j \ge 0\)) be the α-Stirling entries of \(\alpha\). Then for all \(i, j \ge 0\), \(s_{i+1,j+1} = s_{i,j} + \alpha_{j+2} s_{i,j+1}\).

theorem alphaStirlingEntry_succ_succ (α : ℕ → R) (i j : ℕ) :
    alphaStirlingEntry α (i + 1) (j + 1) =
      alphaStirlingEntry α i j + α (j + 2) * alphaStirlingEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, equation (a-1).

Uses 1

Statement usesEntries of the α-Stirling matrix

TheoremFirst column of the α-Stirling entries#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(s_{i,j}\) (\(i, j \ge 0\)) be the α-Stirling entries of \(\alpha\). Then \(s_{i,0} = \alpha_1\) for every \(i \ge 0\).

theorem alphaStirlingEntry_zero_right (α : ℕ → R) (i : ℕ) : alphaStirlingEntry α i 0 = α 1

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, equation (a-1).

Uses 1

Statement usesEntries of the α-Stirling matrix

TheoremRecurrence for the shifted α-Stirling entries#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha = (\alpha_j)_{j \ge 1}\) be a sequence in \(R\), and write \(\mathsf{S}_{i,j}\) for the entries of the shifted \(\alpha\)-Stirling matrix of \(\alpha\), indexed from \(0\). For all natural numbers \(i\) and \(j\),

\[\mathsf{S}_{i+1,j+1} = \mathsf{S}_{i+1,j} + \alpha_{j+2} \mathsf{S}_{i,j+1}.\]

theorem shiftedAlphaStirlingEntry_succ_succ (α : ℕ → R) (i j : ℕ) :
    shiftedAlphaStirlingEntry α (i + 1) (j + 1) =
      shiftedAlphaStirlingEntry α (i + 1) j + α (j + 2) * shiftedAlphaStirlingEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4.

Uses 1

Statement usesEntries of the shifted α-Stirling matrix

TheoremFirst row of the shifted α-Stirling matrix#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha = (\alpha_j)_{j \ge 1}\) be a sequence in \(R\), and write \(\mathsf{S}_{i,j}\) for the entries of the shifted \(\alpha\)-Stirling matrix of \(\alpha\), indexed from \(0\). For every natural number \(j\), \(\mathsf{S}_{0,j} = \alpha_1\); that is, the first row is constant, equal to \(\alpha_1\).

theorem shiftedAlphaStirlingEntry_zero_left (α : ℕ → R) (j : ℕ) :
    shiftedAlphaStirlingEntry α 0 j = α 1

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4.

Uses 1

Statement usesEntries of the shifted α-Stirling matrix

TheoremRecurrence for the α-upper entries#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(u_{i,j}\) (\(i, j \ge 0\)) be the α-upper entries of \(\alpha\). Then for all \(i, j \ge 0\), \(u_{i+1,j+1} = u_{i+1,j} + \alpha_{i+1} u_{i,j} + (\alpha_{j+2} - \alpha_{i+1}) u_{i,j+1}\).

theorem alphaUpperEntry_succ_succ (α : ℕ → R) (i j : ℕ) :
    alphaUpperEntry α (i + 1) (j + 1) =
      alphaUpperEntry α (i + 1) j + α (i + 1) * alphaUpperEntry α i j +
        (α (j + 2) - α (i + 1)) * alphaUpperEntry α i (j + 1)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, equation (u-1-2).

Uses 1

Statement usesEntries of the α-upper matrix

TheoremSmall α-upper entries#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(u_{i,j}\) (\(i, j \ge 0\)) be the α-upper entries of \(\alpha\). Then \(u_{1,1} = \alpha_2\) and \(u_{1,2} = \alpha_2 + \alpha_3\).

Writing \(\mathsf{U}_{i,j}\) for the entries of the paper's matrix \(\mathsf{U}_\alpha(n)\) in its \(1\)-based indexing, these are \(\mathsf{U}_{2,2} = \alpha_2\) and \(\mathsf{U}_{2,3} = \alpha_2 + \alpha_3\), as in the paper's display of \(\mathsf{U}_\alpha(4)\).

theorem alphaUpperEntry_one_one_one_two (α : ℕ → R) :
    alphaUpperEntry α 1 1 = α 2 ∧ alphaUpperEntry α 1 2 = α 2 + α 3

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 2.

Uses 1

Statement usesEntries of the α-upper matrix

DefinitionThe α-Stirling matrix#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(s_{i,j}\) (\(i, j \ge 0\)) be the α-Stirling entries of \(\alpha\). For \(n \ge 0\), the matrix \(S_\alpha(n)\) is the \(n \times n\) matrix over \(R\), with rows and columns indexed by \(0, 1, \dots, n - 1\), whose \((i, j)\) entry is \(s_{i,j}\).

def alphaStirlingMatrix (α : ℕ → R) (n : ℕ) : Matrix (Fin n) (Fin n) R :=
  Matrix.of fun a b => alphaStirlingEntry α a b

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4.

Uses 1 · Used by 1

Statement usesEntries of the α-Stirling matrix

Used byLU decomposition of the shifted α-Stirling matrix

DefinitionShifted α-Stirling matrix#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha = (\alpha_j)_{j \ge 1}\) be a sequence in \(R\), and let \(n\) be a natural number. The shifted \(\alpha\)-Stirling matrix \(\mathsf{S}_\alpha(n)\) is the \(n \times n\) matrix over \(R\) whose entry in row \(i\) and column \(j\) (counted from \(0\)) is the shifted \(\alpha\)-Stirling entry \(\mathsf{S}_{i,j}\), given by \(\mathsf{S}_{i,0} = \mathsf{S}_{0,j} = \alpha_1\) and \(\mathsf{S}_{i+1,j+1} = \mathsf{S}_{i+1,j} + \alpha_{j+2} \mathsf{S}_{i,j+1}\).

def shiftedAlphaStirlingMatrix (α : ℕ → R) (n : ℕ) : Matrix (Fin n) (Fin n) R :=
  Matrix.of fun a b => shiftedAlphaStirlingEntry α a b

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 1.4.

Uses 1 · Used by 2

Statement usesEntries of the shifted α-Stirling matrix

Used byDeterminant of the shifted \(\alpha\)-Stirling matrix · LU decomposition of the shifted α-Stirling matrix

DefinitionThe α-upper matrix#✓fully proved

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(u_{i,j}\) (\(i, j \ge 0\)) be the α-upper entries of \(\alpha\). For \(n \ge 0\), the matrix \(\mathsf{U}_\alpha(n)\) is the \(n \times n\) matrix over \(R\), with rows and columns indexed by \(0, 1, \dots, n - 1\), whose \((i, j)\) entry is \(u_{i,j}\).

def alphaUpperMatrix (α : ℕ → R) (n : ℕ) : Matrix (Fin n) (Fin n) R :=
  Matrix.of fun a b => alphaUpperEntry α a b

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 2.

Uses 1 · Used by 2

Statement usesEntries of the α-upper matrix

Used byDeterminant of the α-upper matrix · LU decomposition of the shifted α-Stirling matrix

Theoremα-upper entries are complete homogeneous symmetric polynomials#●ready to prove

Let \(R\) be a commutative ring, let \(\alpha\) be a sequence in \(R\), and let \(u_{i,j}\) (\(i, j \ge 0\)) be the α-upper entries of \(\alpha\). For all \(i \le j\), \(u_{i,j} = h_i(\alpha_{i+1}, \alpha_{i+2}, \dots, \alpha_{j+1})\), where \(h_i\) is the complete homogeneous symmetric polynomial of degree \(i\) in \(j - i + 1\) variables.

Writing \(\mathsf{U}_{i,j}\) for the entries of the paper's matrix \(\mathsf{U}_\alpha(n)\) in its \(1\)-based indexing, this reads \(\mathsf{U}_{i,j} = h_{i-1}(\alpha_i, \dots, \alpha_j)\) for \(j \ge i \ge 1\).

public theorem_wanted alphaUpperEntry_eq_hsymm (α : ℕ → R) {i j : ℕ} (hij : i ≤ j) :
    alphaUpperEntry α i j =
      MvPolynomial.eval (fun t : Fin (j - i + 1) => α (i + 1 + t))
        (MvPolynomial.hsymm (Fin (j - i + 1)) R i)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Lemma 1 (jis-2026-26.5.4-lem-1).

Uses 1

Statement usesEntries of the α-upper matrix

TheoremDeterminant of the α-upper matrix#●ready to prove

Let \(R\) be a commutative ring and let \(\alpha\) be a sequence in \(R\). For every \(n \ge 0\), the determinant of the \(n \times n\) α-upper matrix \(\mathsf{U}_\alpha(n)\) is \(\det \mathsf{U}_\alpha(n) = \prod_{i=1}^{n} \alpha_i^{i-1}\).

public theorem_wanted det_alphaUpperMatrix (α : ℕ → R) (n : ℕ) :
    (alphaUpperMatrix α n).det = ∏ i : Fin n, α (i + 1) ^ (i : ℕ)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Lemma 1 (jis-2026-26.5.4-lem-1).

Uses 1

Statement usesThe α-upper matrix

TheoremLU decomposition of the shifted α-Stirling matrix#●ready to prove

Let \(R\) be a commutative ring, let \(\alpha = (\alpha_j)_{j \ge 1}\) be a sequence in \(R\), and let \(n\) be a natural number. Then

\[\mathsf{S}_\alpha(n) = S_\alpha(n) \mathsf{U}_\alpha(n),\]

where \(\mathsf{S}_\alpha(n)\) is the \(n \times n\) shifted \(\alpha\)-Stirling matrix, \(S_\alpha(n)\) is the \(n \times n\) \(\alpha\)-Stirling matrix and \(\mathsf{U}_\alpha(n)\) is the \(n \times n\) upper matrix of \(\alpha\).

The paper assumes \(\alpha_1 = 1\). The identity holds for every sequence \(\alpha\) because both sides scale by \(\alpha_1\) and \(\mathsf{U}_\alpha(n)\) does not depend on \(\alpha_1\).

public theorem_wanted shiftedAlphaStirlingMatrix_eq_mul (α : ℕ → R) (n : ℕ) :
    shiftedAlphaStirlingMatrix α n = alphaStirlingMatrix α n * alphaUpperMatrix α n

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 2 (jis-2026-26.5.4-thm-2).

Uses 3

Statement usesThe α-Stirling matrix · The α-upper matrix · Shifted α-Stirling matrix

TheoremDeterminant of the shifted \(\alpha\)-Stirling matrix#●ready to prove

Let \(R\) be a commutative ring and let \((\alpha_j)_{j \ge 1}\) be a sequence in \(R\) with \(\alpha_1 = 1\). For \(n \ge 0\) let \(\mathsf{S}_\alpha(n)\) be the \(n \times n\) matrix whose \((i, j)\) entry \(\mathsf{S}_{i,j}\), with rows and columns indexed from \(1\), is \(\alpha_1\) when \(i = 1\) or \(j = 1\), and satisfies \(\mathsf{S}_{i,j} = \mathsf{S}_{i,j-1} + \alpha_j \mathsf{S}_{i-1,j}\) for \(i, j \ge 2\). Then \(\det \mathsf{S}_\alpha(n) = \prod_{j=1}^{n} \alpha_j^{\,j-1}\).

public theorem_wanted det_shiftedAlphaStirlingMatrix (α : ℕ → R) (hα : α 1 = 1) (n : ℕ) :
    (shiftedAlphaStirlingMatrix α n).det = ∏ j : Fin n, α (j + 1) ^ (j : ℕ)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 2 (jis-2026-26.5.4-thm-2).

Uses 1

Statement usesShifted α-Stirling matrix

DefinitionPascal diagonal matrices#✓fully proved

For \(m, n \ge 0\), \(\mathsf{L}_{d^{(m)}}(n)\) is the \(n \times n\) real matrix that carries the \(m\)-th diagonal \(d^{(m)}_b = \binom{m+b}{b}\) (\(b \ge 0\)) of Pascal's triangle on its \(m\)-th subdiagonal: with rows and columns indexed from \(0\), its \((b + m, b)\) entry is \(\binom{m+b}{b}\) for every \(b\) with \(b + m < n\), and all its other entries are \(0\).

def pascalDiagonalMatrix (m n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun a b => if (a : ℕ) = b + m then ((m + b).choose b : ℝ) else 0

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 3.

Used by 2

Used byExponential of a Pascal diagonal matrix · The zeroth Pascal diagonal matrix is the identity

TheoremThe zeroth Pascal diagonal matrix is the identity#✓fully proved

For \(m, n \ge 0\) let \(\mathsf{L}_{d^{(m)}}(n)\) be the \(n \times n\) real matrix whose \((b + m, b)\) entry is \(\binom{m+b}{b}\) for each \(b\) with \(b + m < n\) and whose other entries are \(0\), with rows and columns indexed from \(0\). Then \(\mathsf{L}_{d^{(0)}}(n) = I_n\), the \(n \times n\) identity matrix, for every \(n \ge 0\).

theorem pascalDiagonalMatrix_zero (n : ℕ) : pascalDiagonalMatrix 0 n = 1

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 3.

Uses 1

Statement usesPascal diagonal matrices

DefinitionFirst-column sequence for exponentials of Pascal diagonal matrices#✓fully proved

For \(k \ge 0\), the sequence of natural numbers \(\alpha^{(k)} = (\alpha^{(k)}_i)_{i \ge 0}\) is defined by \(\alpha^{(k)}_0 = 0\), \(\alpha^{(k)}_1 = 1\) and, for \(i \ge 2\), \(\alpha^{(k)}_i = \binom{i-2}{k-1} \alpha^{(k)}_{i-k}\) if \(1 \le k < i\) and \(\alpha^{(k)}_i = 0\) otherwise. Thus \(\alpha^{(k)}_i = 0\) for \(2 \le i \le k\), and \(\alpha^{(0)}_i = 0\) for all \(i \ne 1\).

def pascalExpFirstColumn (k i : ℕ) : ℕ :=
  if i = 1 then 1
  else if _h : 0 < k ∧ k < i then (i - 2).choose (k - 1) * pascalExpFirstColumn k (i - k)
  else 0
termination_by i
decreasing_by omega

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 3.

Used by 4

Used byExponential of a Pascal diagonal matrix · Vanishing terms of the Pascal first-column sequence · Recurrence for the Pascal first-column sequence · First term of the Pascal first-column sequence

TheoremFirst term of the Pascal first-column sequence#✓fully proved

For every \(k \ge 0\), the first-column sequence \(\alpha^{(k)}\) satisfies \(\alpha^{(k)}_1 = 1\).

theorem pascalExpFirstColumn_one (k : ℕ) : pascalExpFirstColumn k 1 = 1

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 3.

Uses 1

Statement usesFirst-column sequence for exponentials of Pascal diagonal matrices

TheoremVanishing terms of the Pascal first-column sequence#✓fully proved

For all natural numbers \(k\) and \(i\) with \(2 \le i \le k\), the first-column sequence \(\alpha^{(k)}\) satisfies \(\alpha^{(k)}_i = 0\).

theorem pascalExpFirstColumn_of_le {k i : ℕ} (h2 : 2 ≤ i) (hik : i ≤ k) :
    pascalExpFirstColumn k i = 0

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 3.

Uses 1

Statement usesFirst-column sequence for exponentials of Pascal diagonal matrices

TheoremRecurrence for the Pascal first-column sequence#✓fully proved

For all natural numbers \(k\) and \(i\) with \(1 \le k < i\), the first-column sequence \(\alpha^{(k)}\) satisfies \(\alpha^{(k)}_i = \binom{i-2}{k-1} \alpha^{(k)}_{i-k}\).

theorem pascalExpFirstColumn_of_lt {k i : ℕ} (hk : 1 ≤ k) (hki : k < i) :
    pascalExpFirstColumn k i = (i - 2).choose (k - 1) * pascalExpFirstColumn k (i - k)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 3.

Uses 1

Statement usesFirst-column sequence for exponentials of Pascal diagonal matrices

TheoremExponential of a Pascal diagonal matrix#●ready to prove

Let \(k \ge 1\) and \(n \ge 0\). For \(m \ge 0\) let \(\mathsf{L}_{d^{(m)}}(n)\) be the \(n \times n\) real matrix whose \((b + m, b)\) entry is \(\binom{m+b}{b}\) for each \(b\) with \(b + m < n\) and whose other entries are \(0\) (indices from \(0\)). Let \(\alpha^{(k)} = (\alpha^{(k)}_i)_{i \ge 1}\) be given by \(\alpha^{(k)}_1 = 1\), \(\alpha^{(k)}_i = 0\) for \(2 \le i \le k\) and \(\alpha^{(k)}_i = \binom{i-2}{k-1} \alpha^{(k)}_{i-k}\) for \(i > k\), and let \(T_{\alpha^{(k)}, \beta}(n)\) be the \(n \times n\) lower triangular Toeplitz matrix with first column \(\alpha^{(k)}\) and first row \(\beta = (1, 0, 0, \ldots)\), that is, with \((a, b)\) entry \(\alpha^{(k)}_{a-b+1}\) for \(b \le a\) and \(0\) for \(b > a\). Then \(\exp(\mathsf{L}_{d^{(k)}}(n))\) equals the Hadamard (entrywise) product \(T_{\alpha^{(k)}, \beta}(n) \odot \sum_{i=0}^{n-1} \mathsf{L}_{d^{(ki)}}(n)\).

The paper sums over all \(i \ge 0\); the terms with \(i \ge n\) are zero matrices, since then \(ki \ge n\).

public theorem_wanted exp_pascalDiagonalMatrix (k : ℕ) (hk : 1 ≤ k) (n : ℕ) :
    NormedSpace.exp (pascalDiagonalMatrix k n) =
      (Matrix.of fun a b : Fin n =>
          if (b : ℕ) ≤ a then (pascalExpFirstColumn k ((a : ℕ) - b + 1) : ℝ) else 0) ⊙
        ∑ i ∈ Finset.range n, pascalDiagonalMatrix (k * i) n

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 3 (jis-2026-26.5.4-thm-3).

Uses 2

Statement usesPascal diagonal matrices · First-column sequence for exponentials of Pascal diagonal matrices

DefinitionFactorial matrix of a power series#✓fully proved

Let \(K\) be a field, let \(f\) be a formal power series over \(K\) in the variable \(t\), and let \(n\) be a natural number. The factorial matrix \(M_n(f)\) is the \(n \times n\) matrix over \(K\) whose entry in row \(a\) and column \(b\) (counted from \(0\)) is \((a! \cdot 1_K) / (b! \cdot 1_K)\) times the coefficient of \(t^{a-b}\) in \(f\) when \(b \le a\), and \(0\) when \(b > a\). Here the quotient is taken in \(K\) and is read as \(0\) when \(b! \cdot 1_K = 0\), which can happen only in positive characteristic. When \(K\) has characteristic zero, the factor is the integer \(a!/b!\) and \(M_n(f)\) is the leading \(n \times n\) section of the infinite lower triangular matrix \(M(f)\) of Moghaddamfar, Salehy and Salehy.

noncomputable def powerSeriesFactorialMatrix {K : Type*} [Field K] (f : PowerSeries K) (n : ℕ) :
    Matrix (Fin n) (Fin n) K :=
  Matrix.of fun a b =>
    if (b : ℕ) ≤ a then
      ((a : ℕ).factorial : K) / ((b : ℕ).factorial : K) * PowerSeries.coeff ((a : ℕ) - b) f
    else 0

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 3.

Used by 2

Used byDiagonal of the factorial matrix of a power series · Multiplicativity of the factorial matrix of a power series

TheoremDiagonal of the factorial matrix of a power series#✓fully proved

Let \(K\) be a field of characteristic zero, let \(f\) be a formal power series over \(K\) and let \(n \ge 0\). Every diagonal entry of the leading \(n \times n\) section of \(M(f)\), the lower triangular matrix whose \((a, b)\) entry, with rows and columns indexed from \(0\), is \(\frac{a!}{b!} [t^{a-b}] f\) for \(b \le a\) and \(0\) for \(b > a\), equals the constant coefficient \([t^0] f\) of \(f\).

theorem powerSeriesFactorialMatrix_apply_self {K : Type*} [Field K] [CharZero K]
    (f : PowerSeries K) (n : ℕ) (a : Fin n) :
    powerSeriesFactorialMatrix f n a a = PowerSeries.coeff 0 f

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Section 3.

Uses 1

Statement usesFactorial matrix of a power series

TheoremMultiplicativity of the factorial matrix of a power series#●ready to prove

Let \(K\) be a field of characteristic zero, let \(f\) and \(g\) be formal power series over \(K\) in the variable \(t\), and let \(n\) be a natural number. For a power series \(h\) over \(K\), write \(M_n(h)\) for the \(n \times n\) factorial matrix of \(h\), whose entry in row \(a\) and column \(b\) (counted from \(0\)) is \(\frac{a!}{b!}\) times the coefficient of \(t^{a-b}\) in \(h\) when \(b \le a\), and \(0\) otherwise. Then \(M_n(f) M_n(g) = M_n(fg)\).

Since these matrices are lower triangular and \(M_n(h)\) is the leading \(n \times n\) section of the infinite matrix \(M(h)\), this is equivalent to \(M(f) M(g) = M(fg)\).

public theorem_wanted powerSeriesFactorialMatrix_mul {K : Type*} [Field K] [CharZero K]
    (f g : PowerSeries K) (n : ℕ) :
    powerSeriesFactorialMatrix f n * powerSeriesFactorialMatrix g n =
      powerSeriesFactorialMatrix (f * g) n

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Lemma 5 (jis-2026-26.5.4-lem-5).

Uses 1

Statement usesFactorial matrix of a power series

TheoremBanded Hessenberg–Toeplitz determinants and linear recurrences#●ready to prove

Let \(R\) be a commutative ring, let \(k \ge 1\), and let \((c_j)_{j \ge 1}\) and \((\beta_m)_{m \ge 1}\) be sequences in \(R\) such that \(\beta_1 = \cdots = \beta_{k-1} = 0\), \(\beta_k = 1\) and \(\beta_m = \sum_{j=1}^{k} c_j \beta_{m-j}\) for every \(m > k\). For \(n \ge 0\) let \(H_n\) be the \(n \times n\) upper Hessenberg Toeplitz matrix whose \((i, j)\) entry is \(c_{j-i+1}\) if \(0 \le j - i \le k - 1\), is \(-1\) if \(i = j + 1\), and is \(0\) otherwise. Then \(\det H_n = \beta_{n+k}\).

Unlike the paper, this is stated over any commutative ring, without the assumption \(c_k \ne 0\), and also for \(n = 0\).

public theorem_wanted det_hessenbergToeplitz_eq_recurrence (k : ℕ) (hk : 1 ≤ k) (c β : ℕ → R)
    (hβ : ∀ i, 1 ≤ i → i < k → β i = 0) (hβk : β k = 1)
    (hrec : ∀ m, k < m → β m = ∑ j ∈ Finset.Icc 1 k, c j * β (m - j)) (n : ℕ) :
    (Matrix.of fun a b : Fin n =>
        if (a : ℕ) ≤ b ∧ (b : ℕ) - a < k then c ((b : ℕ) - a + 1)
        else if (a : ℕ) = b + 1 then -1 else 0).det = β (n + k)

Sources

• A. R. Moghaddamfar, Navid Salehy and Nima Salehy, A Generalization of the Pascal and Stirling Matrices, Journal of Integer Sequences 29 (2026), Article 26.5.4, Theorem 7 (jis-2026-26.5.4-thm-7).

DefinitionEntries of the Stirling-like matrix \(S_\alpha\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals, the numbers \(S_{i,j}\) for natural numbers \(i, j\) are defined recursively by \(S_{1,j} = \alpha_{j-1}\) for \(j \ge 1\), \(S_{i,1} = \alpha_0\) for \(i \ge 2\), \(S_{i,j} = S_{i-1,j-1} + j \, S_{i-1,j}\) for \(i, j \ge 2\), and \(S_{i,j} = 0\) when \(i = 0\) or \(j = 0\).

def stirlingLikeEntry (α : ℕ → ℚ) : ℕ → ℕ → ℚ
  | 0, _ => 0
  | 1, j => if j = 0 then 0 else α (j - 1)
  | i + 2, j =>
      if j = 1 then α 0
      else if j = 0 then 0
      else stirlingLikeEntry α (i + 1) (j - 1) +
        (j : ℚ) * stirlingLikeEntry α (i + 1) j

Used by 1

Used byStirling-like matrix

DefinitionEntries of the matrix \(U_\alpha\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rational numbers, the entries \(U_{i,j}\) (\(i, j \ge 1\)) of the matrix \(U_\alpha\) are defined by recursion on the row index \(i\). The first row is \(U_{1,j} = \alpha_{j-1}\). For \(i \ge 2\) the first column is \(U_{i,1} = 0\), and for \(j \ge 2\)

\[U_{i,j} = U_{i-1,j-1} + (j - i + 1)\, U_{i-1,j}.\]

Entries with \(i = 0\) or \(j = 0\) are set to \(0\).

def uEntry (α : ℕ → ℚ) : ℕ → ℕ → ℚ
  | 0, _ => 0
  | 1, j => if j = 0 then 0 else α (j - 1)
  | i + 2, j =>
      if j ≤ 1 then 0
      else uEntry α (i + 1) (j - 1) +
        ((j : ℚ) - (i + 2) + 1) * uEntry α (i + 1) j

Used by 3

Used byExplicit formula for the entries of \(U_\alpha\) · The matrix \(U_\alpha\) is upper triangular · The matrix \(U_\alpha(n)\)

DefinitionThe sum \(\Psi_\alpha(k)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and a natural number \(k\), \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \frac{\alpha_l}{(k-1-l)!}\); in particular \(\Psi_\alpha(0) = 0\).

def psi (α : ℕ → ℚ) (k : ℕ) : ℚ :=
  ∑ l ∈ Finset.range k, α l / (k - 1 - l).factorial

Used by 3

Used byEntries of the matrix \(R_\alpha\) · First-kind Stirling formula for \(\Lambda(\alpha, i, j)\) · Second-kind Stirling transform of the \(\Lambda\) coefficients

DefinitionThe sum \(\Omega(\alpha, j)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and a natural number \(j\), \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), where \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) is the falling factorial; in particular \(\Omega(\alpha, 0) = 0\).

def omega (α : ℕ → ℚ) (j : ℕ) : ℚ :=
  ∑ l ∈ Finset.range j,
    (Nat.descFactorial (j - 1) l : ℚ) * α l

Used by 4

Used byEntries of the matrix \(\tilde R_\alpha\) · The inverse of the matrix \(R_\alpha(n)\) · Determinant of the Stirling-like matrix · Stirling and falling-factorial sum of the \(\Lambda\) coefficients

DefinitionThe sum \(\Lambda(\alpha, k_1, k_2)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and natural numbers \(k_1, k_2\),

\[ \Lambda(\alpha, k_1, k_2) = \sum_{l=0}^{k_1-1} \binom{k_1-1}{l} \frac{(l+k_2-k_1)!}{(k_2-k_1)!} \, \alpha_{l+k_2-k_1}, \]

where differences of natural numbers are truncated at \(0\) (this matters only when \(k_2 < k_1\)).

def lambda (α : ℕ → ℚ) (k₁ k₂ : ℕ) : ℚ :=
  ∑ l ∈ Finset.range k₁, (Nat.choose (k₁ - 1) l : ℚ) *
    ((l + k₂ - k₁).factorial : ℚ) / (k₂ - k₁).factorial *
    α (l + k₂ - k₁)

Used by 4

Used byFirst-kind Stirling formula for \(\Lambda(\alpha, i, j)\) · Stirling and falling-factorial sum of the \(\Lambda\) coefficients · Second-kind Stirling transform of the \(\Lambda\) coefficients · Explicit formula for the entries of \(U_\alpha\)

DefinitionEntries of the matrix \(R_\alpha\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and natural numbers \(i, j\), the entry \(R_{i,j}\) is \(\frac{(-1)^{j-i}}{(j-i)!} \Psi_\alpha(i)\) if \(i \le j\) and \(0\) if \(i > j\), where \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \frac{\alpha_l}{(k-1-l)!}\). The matrix \(R_\alpha\) uses the indices \(i, j \ge 1\).

def rEntry (α : ℕ → ℚ) (i j : ℕ) : ℚ :=
  if i ≤ j then (-1 : ℚ) ^ (j - i) / (j - i).factorial * psi α i
  else 0

Uses 1 · Used by 2

Statement usesThe sum \(\Psi_\alpha(k)\)

Used byThe matrix \(R_\alpha(n)\) · Column sums of the matrix \(R_\alpha\)

DefinitionEntries of the matrix \(\tilde R_\alpha\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and natural numbers \(i, j\), the entry \(\tilde R_{i,j}\) is \((j-1)^{\underline{i-1}} / \Omega(\alpha, j)\) if \(i \le j\) and \(0\) if \(i > j\), where \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) is the falling factorial, \(0 - 1\) is read as \(0\), and division by \(0\) gives \(0\). The matrix \(\tilde R_\alpha\) uses the indices \(i, j \ge 1\).

def rTildeEntry (α : ℕ → ℚ) (i j : ℕ) : ℚ :=
  if i ≤ j then
    (Nat.descFactorial (j - 1) (i - 1) : ℚ) / omega α j
  else 0

Uses 1 · Used by 1

Statement usesThe sum \(\Omega(\alpha, j)\)

Used byThe matrix \(\tilde R_\alpha(n)\)

DefinitionStirling-like matrix#✓fully proved

For a sequence \(\alpha \colon \mathbb{N} \to \mathbb{Q}\) and \(n \in \mathbb{N}\), the Stirling-like matrix \(S_\alpha(n)\) is the \(n \times n\) rational matrix, with rows and columns indexed by \(1, \dots, n\), whose \((i, j)\) entry is \(S_{i,j}\), where \(S_{1,j} = \alpha_{j-1}\) for \(j \ge 1\), \(S_{i,1} = \alpha_0\) for \(i \ge 2\), and \(S_{i,j} = S_{i-1,j-1} + j \, S_{i-1,j}\) for \(i, j \ge 2\).

def stirlingLikeMatrix (α : ℕ → ℚ) (n : ℕ) :
    Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b => stirlingLikeEntry α (a.val + 1) (b.val + 1)

Uses 1 · Used by 2

Statement usesEntries of the Stirling-like matrix \(S_\alpha\)

Used byTwo factorizations of the Stirling-like matrix · Determinant of the Stirling-like matrix

DefinitionThe matrix \(U_\alpha(n)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and a natural number \(n\), \(U_\alpha(n)\) is the \(n \times n\) rational matrix whose \((i, j)\) entry, for \(1 \le i, j \le n\), is \(U_{i,j}\), where \(U_{1,j} = \alpha_{j-1}\) for \(j \ge 1\), \(U_{i,1} = 0\) for \(i \ge 2\), and \(U_{i,j} = U_{i-1,j-1} + (j - i + 1) \, U_{i-1,j}\) for \(i, j \ge 2\).

def uMatrix (α : ℕ → ℚ) (n : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b => uEntry α (a.val + 1) (b.val + 1)

Uses 1 · Used by 1

Statement usesEntries of the matrix \(U_\alpha\)

Used byTwo factorizations of the Stirling-like matrix

DefinitionThe matrix \(R_\alpha(n)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and a natural number \(n\), \(R_\alpha(n)\) is the \(n \times n\) rational matrix whose \((i, j)\) entry, for \(1 \le i, j \le n\), is \(\frac{(-1)^{j-i}}{(j-i)!} \Psi_\alpha(i)\) if \(i \le j\) and \(0\) if \(i > j\), where \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \frac{\alpha_l}{(k-1-l)!}\).

def rMatrix (α : ℕ → ℚ) (n : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b => rEntry α (a.val + 1) (b.val + 1)

Uses 1 · Used by 2

Statement usesEntries of the matrix \(R_\alpha\)

Used byThe inverse of the matrix \(R_\alpha(n)\) · Two factorizations of the Stirling-like matrix

DefinitionThe matrix \(\tilde R_\alpha(n)\)#✓fully proved

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals and a natural number \(n\), \(\tilde R_\alpha(n)\) is the \(n \times n\) rational matrix whose \((i, j)\) entry, for \(1 \le i, j \le n\), is \((j-1)^{\underline{i-1}} / \Omega(\alpha, j)\) if \(i \le j\) and \(0\) if \(i > j\), where \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) is the falling factorial, and division by \(0\) gives \(0\).

def rTildeMatrix (α : ℕ → ℚ) (n : ℕ) :
    Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b => rTildeEntry α (a.val + 1) (b.val + 1)

Uses 1 · Used by 1

Statement usesEntries of the matrix \(\tilde R_\alpha\)

Used byThe inverse of the matrix \(R_\alpha(n)\)

DefinitionStirling matrix of the second kind#✓fully proved

For \(n \in \mathbb{N}\), the Stirling matrix of the second kind \(S(n)\) is the \(n \times n\) rational matrix, with rows and columns indexed by \(1, \dots, n\), whose \((i, j)\) entry is the Stirling number of the second kind \(S(i, j)\), the number of partitions of an \(i\)-element set into \(j\) nonempty blocks.

def stirlingMatrix2 (n : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b =>
    (Nat.stirlingSecond (a.val + 1) (b.val + 1) : ℚ)

Used by 5

Used byTwo factorizations of the Stirling-like matrix · Stirling matrix of the second kind times \(V(n) - I_n\) · Stirling matrix of the second kind times powers of \(V(n) - I_n\) · Factorization and determinant of shifted Stirling matrices · Shift zero gives the Stirling matrix of the second kind

DefinitionThe Vandermonde matrix \(V(n)\)#✓fully proved

For \(n \in \mathbb{N}\), \(V(n)\) is the \(n \times n\) rational matrix whose entry in row \(i\) and column \(j\) (\(1 \le i, j \le n\)) is \(V_{i,j} = j^{i-1}\).

def vandermondeMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun a b => ((b.val + 1 : ℕ) : ℚ) ^ a.val

Used by 1

Used byTwo factorizations of the Stirling-like matrix

TheoremExplicit formula for the entries of \(U_\alpha\)#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\) and let \(U_\alpha = (U_{i,j})_{i \ge 1, j \ge 0}\) be given by \(U_{i,0} = 0\), \(U_{1,j} = \alpha_{j-1}\) for \(j \ge 1\), \(U_{i,1} = 0\) for \(i \ge 2\), and \(U_{i,j} = U_{i-1,j-1} + (j-i+1) \, U_{i-1,j}\) for \(i, j \ge 2\). For \(k_1 \le k_2\) let \(\Lambda(\alpha, k_1, k_2) = \sum_{l=0}^{k_1-1} \binom{k_1-1}{l} \frac{(l+k_2-k_1)!}{(k_2-k_1)!} \, \alpha_{l+k_2-k_1}\). Then \(U_{i,j} = \Lambda(\alpha, i, j)\) for all \(1 \le i \le j\).

theorem_wanted uEntry_eq_lambda (α : ℕ → ℚ) (i j : ℕ)
    (hi : 1 ≤ i) (hij : i ≤ j) :
    uEntry α i j = lambda α i j

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Lemma 1.

Uses 2

Statement usesThe sum \(\Lambda(\alpha, k_1, k_2)\) · Entries of the matrix \(U_\alpha\)

TheoremThe matrix \(U_\alpha\) is upper triangular#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\) and let \(U_\alpha = (U_{i,j})_{i \ge 1, j \ge 0}\) be given by \(U_{i,0} = 0\), \(U_{1,j} = \alpha_{j-1}\) for \(j \ge 1\), \(U_{i,1} = 0\) for \(i \ge 2\), and \(U_{i,j} = U_{i-1,j-1} + (j-i+1) \, U_{i-1,j}\) for \(i, j \ge 2\). Then \(U_{i,j} = 0\) for all natural numbers \(j < i\).

theorem_wanted uEntry_eq_zero_of_lt (α : ℕ → ℚ) (i j : ℕ)
    (h : j < i) :
    uEntry α i j = 0

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Lemma 1.

Uses 1

Statement usesEntries of the matrix \(U_\alpha\)

TheoremColumn sums of the matrix \(R_\alpha\)#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\), let \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \alpha_l / (k-1-l)!\), and let \(R_\alpha\) be the matrix with entries \(R_{i,j} = \frac{(-1)^{j-i}}{(j-i)!} \Psi_\alpha(i)\) for \(1 \le i \le j\) and \(R_{i,j} = 0\) for \(i > j\). Then for every \(j \ge 1\), \(\sum_{i=1}^{j} R_{i,j} = \alpha_{j-1}\).

theorem_wanted sum_rEntry_col (α : ℕ → ℚ) (j : ℕ)
    (hj : 1 ≤ j) :
    ∑ i ∈ Finset.Icc 1 j, rEntry α i j = α (j - 1)

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Lemma 2.

Uses 1

Statement usesEntries of the matrix \(R_\alpha\)

TheoremTwo factorizations of the Stirling-like matrix#●ready to prove

Let \(\alpha = (\alpha_0, \alpha_1, \dots)\) be a sequence of rationals. For natural numbers \(i, j \ge 1\) define \(S_{i,j}\) and \(U_{i,j}\) by \(S_{1,j} = U_{1,j} = \alpha_{j-1}\), \(S_{i,1} = \alpha_0\) and \(U_{i,1} = 0\) for \(i \ge 2\), and, for \(i, j \ge 2\), \(S_{i,j} = S_{i-1,j-1} + j \, S_{i-1,j}\) and \(U_{i,j} = U_{i-1,j-1} + (j-i+1) \, U_{i-1,j}\); let \(R_{i,j} = \frac{(-1)^{j-i}}{(j-i)!} \Psi_\alpha(i)\) if \(i \le j\) and \(R_{i,j} = 0\) if \(i > j\), where \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \frac{\alpha_l}{(k-1-l)!}\). For every natural number \(n\), let \(S_\alpha(n)\), \(U_\alpha(n)\) and \(R_\alpha(n)\) be the \(n \times n\) matrices \((S_{i,j})\), \((U_{i,j})\) and \((R_{i,j})\) with \(1 \le i, j \le n\), let \(S(n) = (S(i,j))_{1 \le i, j \le n}\) be the matrix of Stirling numbers of the second kind, and let \(V(n) = (j^{i-1})_{1 \le i, j \le n}\). Then \(S_\alpha(n) = S(n) \, U_\alpha(n)\) and \(S_\alpha(n) = V(n) \, R_\alpha(n)\).

theorem_wanted stirlingLikeMatrix_decomp (α : ℕ → ℚ)
    (n : ℕ) :
    stirlingLikeMatrix α n = stirlingMatrix2 n * uMatrix α n ∧
      stirlingLikeMatrix α n = vandermondeMatrix n * rMatrix α n

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Theorem 3.

Uses 5

Statement usesThe matrix \(R_\alpha(n)\) · Stirling-like matrix · Stirling matrix of the second kind · The matrix \(U_\alpha(n)\) · The Vandermonde matrix \(V(n)\)

TheoremDeterminant of the Stirling-like matrix#●ready to prove

For a sequence \(\alpha \colon \mathbb{N} \to \mathbb{Q}\) and \(j \ge 1\) let \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), where \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) is the falling factorial. Then for every \(n \in \mathbb{N}\) the determinant of the \(n \times n\) Stirling-like matrix \(S_\alpha(n)\) is \(\det S_\alpha(n) = \prod_{j=1}^{n} \Omega(\alpha, j)\).

theorem_wanted stirlingLikeMatrix_det (α : ℕ → ℚ) (n : ℕ) :
    (stirlingLikeMatrix α n).det =
      ∏ i ∈ Finset.range n, omega α (i + 1)

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Theorem 4.

Uses 2

Statement usesThe sum \(\Omega(\alpha, j)\) · Stirling-like matrix

TheoremSecond-kind Stirling transform of the \(\Lambda\) coefficients#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\), let \(S(i, k)\) denote the Stirling numbers of the second kind, let \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \alpha_l / (k-1-l)!\), and for \(k_1 \le k_2\) let \(\Lambda(\alpha, k_1, k_2) = \sum_{l=0}^{k_1-1} \binom{k_1-1}{l} \frac{(l+k_2-k_1)!}{(k_2-k_1)!} \, \alpha_{l+k_2-k_1}\). Then for all \(i, j \ge 1\),

\[\sum_{k=1}^{\min(i,j)} S(i,k) \, \Lambda(\alpha, k, j) = \sum_{k=1}^{j} k^{i-1} \, \frac{(-1)^{j-k}}{(j-k)!} \, \Psi_\alpha(k).\]

theorem_wanted sum_stirlingSecond_lambda (α : ℕ → ℚ)
    (i j : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) :
    ∑ k ∈ Finset.Icc 1 (min i j),
        (Nat.stirlingSecond i k : ℚ) * lambda α k j =
      ∑ k ∈ Finset.Icc 1 j, (k : ℚ) ^ (i - 1) *
        ((-1 : ℚ) ^ (j - k) / (j - k).factorial) * psi α k

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Proposition 5.

Uses 2

Statement usesThe sum \(\Lambda(\alpha, k_1, k_2)\) · The sum \(\Psi_\alpha(k)\)

TheoremThe inverse of the matrix \(R_\alpha(n)\)#●ready to prove

For a sequence \(\alpha = (\alpha_0, \alpha_1, \dots)\) of rationals, let \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \frac{\alpha_l}{(k-1-l)!}\) and \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), where \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) is the falling factorial. For a natural number \(n\), let \(R_\alpha(n)\) and \(\tilde R_\alpha(n)\) be the upper triangular \(n \times n\) rational matrices whose \((i, j)\) entries for \(1 \le i \le j \le n\) are \(\frac{(-1)^{j-i}}{(j-i)!} \Psi_\alpha(i)\) and \((j-1)^{\underline{i-1}} / \Omega(\alpha, j)\) respectively. If \(\prod_{j=1}^{n} \Omega(\alpha, j) \ne 0\), then \(\tilde R_\alpha(n) = R_\alpha(n)^{-1}\).

theorem_wanted rTildeMatrix_eq_inv (α : ℕ → ℚ) (n : ℕ)
    (h : ∏ j ∈ Finset.Icc 1 n, omega α j ≠ 0) :
    rTildeMatrix α n = (rMatrix α n)⁻¹

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Lemma 7.

Uses 3

Statement usesThe sum \(\Omega(\alpha, j)\) · The matrix \(R_\alpha(n)\) · The matrix \(\tilde R_\alpha(n)\)

TheoremStirling and falling-factorial sum of the \(\Lambda\) coefficients#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\), let \(S(i, k)\) denote the Stirling numbers of the second kind, let \(m^{\underline{l}} = m(m-1)\cdots(m-l+1)\) be the falling factorial, let \(\Omega(\alpha, j) = \sum_{l=0}^{j-1} (j-1)^{\underline{l}} \, \alpha_l\), and for \(k_1 \le k_2\) let \(\Lambda(\alpha, k_1, k_2) = \sum_{l=0}^{k_1-1} \binom{k_1-1}{l} \frac{(l+k_2-k_1)!}{(k_2-k_1)!} \, \alpha_{l+k_2-k_1}\). If \(i, j \ge 1\) and \(\prod_{k=1}^{\max(i,j)} \Omega(\alpha, k) \ne 0\), then

\[\sum_{k_1=1}^{i} \sum_{k_2=k_1}^{j} S(i,k_1) \, (j-1)^{\underline{k_2-1}} \, \Lambda(\alpha, k_1, k_2) = j^{i-1} \, \Omega(\alpha, j).\]

theorem_wanted sum_stirlingSecond_descFactorial_lambda
    (α : ℕ → ℚ) (i j : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j)
    (h : ∏ k ∈ Finset.Icc 1 (max i j), omega α k ≠ 0) :
    ∑ k₁ ∈ Finset.Icc 1 i, ∑ k₂ ∈ Finset.Icc k₁ j,
        (Nat.stirlingSecond i k₁ : ℚ) *
          (Nat.descFactorial (j - 1) (k₂ - 1) : ℚ) *
          lambda α k₁ k₂ =
      (j : ℚ) ^ (i - 1) * omega α j

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Proposition 8.

Uses 2

Statement usesThe sum \(\Lambda(\alpha, k_1, k_2)\) · The sum \(\Omega(\alpha, j)\)

TheoremFirst-kind Stirling formula for \(\Lambda(\alpha, i, j)\)#●ready to prove

Let \(\alpha \colon \mathbb{N} \to \mathbb{Q}\), let \(s(i, k)\) denote the signed Stirling numbers of the first kind, let \(\Psi_\alpha(k) = \sum_{l=0}^{k-1} \alpha_l / (k-1-l)!\), and for \(k_1 \le k_2\) let \(\Lambda(\alpha, k_1, k_2) = \sum_{l=0}^{k_1-1} \binom{k_1-1}{l} \frac{(l+k_2-k_1)!}{(k_2-k_1)!} \, \alpha_{l+k_2-k_1}\). Then for all \(i, j \ge 1\) the sum

\[\sum_{k_1=1}^{i} \sum_{k_2=1}^{j} s(i,k_1) \, k_2^{k_1-1} \, \frac{(-1)^{j-k_2}}{(j-k_2)!} \, \Psi_\alpha(k_2)\]

equals \(\Lambda(\alpha, i, j)\) if \(i \le j\) and \(0\) if \(i > j\).

theorem_wanted sum_signed_psi_eq (α : ℕ → ℚ) (i j : ℕ)
    (hi : 1 ≤ i) (hj : 1 ≤ j) :
    ∑ k₁ ∈ Finset.Icc 1 i, ∑ k₂ ∈ Finset.Icc 1 j,
        (MetaMathlibExt.signedStirlingFirst i k₁ : ℚ) * (k₂ : ℚ) ^ (k₁ - 1) *
          ((-1 : ℚ) ^ (j - k₂) / (j - k₂).factorial) * psi α k₂ =
      if i ≤ j then lambda α i j else 0

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Proposition 9.

Uses 3

Statement usesThe sum \(\Lambda(\alpha, k_1, k_2)\) · The sum \(\Psi_\alpha(k)\) · Signed Stirling numbers of the first kind

TheoremKronecker-delta identity for signed Stirling numbers of the first kind#●ready to prove

Let \(s(i, k)\) denote the signed Stirling numbers of the first kind and \(\delta_{i,j}\) the Kronecker delta (\(1\) if \(i = j\) and \(0\) otherwise). Then for all integers \(i, j \ge 1\), in \(\mathbb{Q}\),

\[\sum_{k_1=1}^{i} \sum_{k_2=1}^{j} \frac{(-1)^{j-k_2} \, s(i,k_1) \, k_2^{k_1-1}}{(j-k_2)! \, (k_2-1)!} = \delta_{i,j}.\]

theorem_wanted sum_signed_eq_delta (i j : ℕ) (hi : 1 ≤ i)
    (hj : 1 ≤ j) :
    ∑ k₁ ∈ Finset.Icc 1 i, ∑ k₂ ∈ Finset.Icc 1 j,
        (-1 : ℚ) ^ (j - k₂) * (MetaMathlibExt.signedStirlingFirst i k₁ : ℚ) *
          (k₂ : ℚ) ^ (k₁ - 1) /
          ((j - k₂).factorial * (k₂ - 1).factorial) =
      if i = j then 1 else 0

Sources

• M. Bahrami-Taghanaki, A. R. Moghaddamfar, Nima Salehy, and Navid Salehy, "Some Identities Involving Stirling Numbers Arising from Matrix Decompositions", Corollary 10.

Uses 1

Statement usesSigned Stirling numbers of the first kind

33 fully proved17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.