Generalized factorial matrices

TheoremGeneralized factorial matrices: decomposition, determinant and inverse#✓fully proved

Let \(K\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(p\) be a natural number, let \(x_0, \dots, x_{p-1} \in K\) be pairwise distinct, and let \(\alpha, \beta, \gamma \in \mathbb{R}\). For \(y \in K\), \(a \in \mathbb{R}\) and \(n \in \mathbb{N}\) write \((y \mid a)_n = \prod_{j=0}^{n-1} (y - ja)\). Let numbers \(S(a, b, c; n, k) \in K\), for \(a, b, c \in \mathbb{R}\) and \(n, k \in \mathbb{N}\), satisfy \(S(a, b, c; n, k) = 0\) whenever \(k > n\), and \((y \mid a)_n = \sum_{k=0}^{n} S(a, b, c; n, k)\,(y - c \mid b)_k\) for all \(a, b, c \in \mathbb{R}\), \(y \in K\) and \(n \in \mathbb{N}\). For \(a, b, c \in \mathbb{R}\) let \(\mathbf{S}(a, b, c)\) be the \(p \times p\) matrix with entries \(S(a, b, c; i, k)\), let \(G_a\) be the \(p \times p\) matrix with entries \((x_k \mid a)_i\), and let \(H\) be the \(p \times p\) matrix with entries \((x_k - \gamma \mid \beta)_i\), where \(0 \le i, k < p\). Then \(G_\alpha = \mathbf{S}(\alpha, \beta, \gamma)\, H\); \(\det G_\alpha = \det G_0\); \(\det G_0 = \prod_{0 \le i < k < p} (x_k - x_i)\); \(G_\alpha\) is invertible; and \(G_\alpha^{-1} = G_0^{-1}\, \mathbf{S}(0, \alpha, 0)\).

This holds for every \(p\), including \(p = 0\).

MetaMathlibExt.pan_vandermonde_general · 31 lines

theorem pan_vandermonde_general
    (p : ℕ)
    (K : Type*) [RCLike K]
    (x : Fin p → K)
    (α β γ : ℝ)
    (S : ℝ → ℝ → ℝ → ℕ → ℕ → K)
    (hS : ∀ (a b c : ℝ) (y : K) (n : ℕ),
      (∏ j ∈ Finset.range n, (y - (j : K) * RCLike.ofReal a)) =
        ∑ k ∈ Finset.range (n + 1),
          S a b c n k * ∏ j ∈ Finset.range k,
            ((y - RCLike.ofReal c) - (j : K) * RCLike.ofReal b))
    (hSvan : ∀ (a b c : ℝ) (n k : ℕ), n < k → S a b c n k = 0)
    (hdist : Function.Injective x) :
    (Matrix.of (fun (r c : Fin p) => ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)) =
      Matrix.of (fun (r c : Fin p) => S α β γ r.val c.val) *
        Matrix.of (fun (r c : Fin p) =>
          ∏ j ∈ Finset.range r.val, ((x c - RCLike.ofReal γ) - (j : K) * RCLike.ofReal β)))
    ∧ Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α))) =
      Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0)))
    ∧ Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0))) =
      ∏ ij ∈ Finset.univ.filter (fun ij : Fin p × Fin p => ij.1 < ij.2), (x ij.2 - x ij.1)
    ∧ IsUnit (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)))
    ∧ (Matrix.of (fun (r c : Fin p) =>
          ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)))⁻¹ =
      (Matrix.of (fun (r c : Fin p) =>
            ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0)))⁻¹ *
        Matrix.of (fun (r c : Fin p) => S 0 α 0 r.val c.val)

Used by 1

Used byPan's theorem on generalized factorial matrices

TheoremPan's theorem on generalized factorial matrices#✓fully proved

Let \(K\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(p\) be a positive integer, let \(x_0, \dots, x_{p-1} \in K\) be pairwise distinct, and let \(\alpha, \beta, \gamma \in \mathbb{R}\). For \(y \in K\), \(a \in \mathbb{R}\) and \(n \in \mathbb{N}\) write \((y \mid a)_n = \prod_{j=0}^{n-1} (y - ja)\). Let numbers \(S(a, b, c; n, k) \in K\), for \(a, b, c \in \mathbb{R}\) and \(n, k \in \mathbb{N}\), satisfy \(S(a, b, c; n, k) = 0\) whenever \(k > n\), and \((y \mid a)_n = \sum_{k=0}^{n} S(a, b, c; n, k)\,(y - c \mid b)_k\) for all \(a, b, c \in \mathbb{R}\), \(y \in K\) and \(n \in \mathbb{N}\). For \(a, b, c \in \mathbb{R}\) let \(\mathbf{S}(a, b, c)\) be the \(p \times p\) matrix with entries \(S(a, b, c; i, k)\), let \(G_a\) be the \(p \times p\) matrix with entries \((x_k \mid a)_i\), and let \(H\) be the \(p \times p\) matrix with entries \((x_k - \gamma \mid \beta)_i\), where \(0 \le i, k < p\). Then \(G_\alpha = \mathbf{S}(\alpha, \beta, \gamma)\, H\); \(\det G_\alpha = \det G_0\); \(\det G_0 = \prod_{0 \le i < k < p} (x_k - x_i)\); \(G_\alpha\) is invertible; and \(G_\alpha^{-1} = G_0^{-1}\, \mathbf{S}(0, \alpha, 0)\).

MetaMathlibExt.pan_vandermonde · 32 lines

theorem pan_vandermonde :
  ∀ (p : ℕ)
    (hp : 0 < p)
    (K : Type*) [RCLike K]
    (x : Fin p → K)
    (α β γ : ℝ)
    (S : ℝ → ℝ → ℝ → ℕ → ℕ → K)
    (hS : ∀ (a b c : ℝ) (y : K) (n : ℕ),
      (∏ j ∈ Finset.range n, (y - (j : K) * RCLike.ofReal a)) =
        ∑ k ∈ Finset.range (n + 1),
          S a b c n k * ∏ j ∈ Finset.range k,
            ((y - RCLike.ofReal c) - (j : K) * RCLike.ofReal b))
    (hSvan : ∀ (a b c : ℝ) (n k : ℕ), n < k → S a b c n k = 0)
    (hdist : Function.Injective x),
    (Matrix.of (fun (r c : Fin p) => ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)) =
      Matrix.of (fun (r c : Fin p) => S α β γ r.val c.val) *
        Matrix.of (fun (r c : Fin p) =>
          ∏ j ∈ Finset.range r.val, ((x c - RCLike.ofReal γ) - (j : K) * RCLike.ofReal β)))
    ∧ Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α))) =
      Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0)))
    ∧ Matrix.det (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0))) =
      ∏ ij ∈ Finset.univ.filter (fun ij : Fin p × Fin p => ij.1 < ij.2), (x ij.2 - x ij.1)
    ∧ IsUnit (Matrix.of (fun (r c : Fin p) =>
        ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)))
    ∧ (Matrix.of (fun (r c : Fin p) =>
          ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal α)))⁻¹ =
      (Matrix.of (fun (r c : Fin p) =>
            ∏ j ∈ Finset.range r.val, (x c - (j : K) * RCLike.ofReal 0)))⁻¹ *
        Matrix.of (fun (r c : Fin p) => S 0 α 0 r.val c.val)

Sources

• Jiaqiang Pan, "Matrix Decomposition of the Unified Generalized Stirling Numbers and Inversion of the Generalized Factorial Matrices," Journal of Integer Sequences 15 (2012), Article 12.6.6, Theorem, lines 428–460, https://cs.uwaterloo.ca/journals/JIS/VOL15/Pan/pan19.tex. It follows from pan_vandermonde_general; the hypothesis hp is unused and keeps the source's shape.

Uses 1

Proof usesGeneralized factorial matrices: decomposition, determinant and inverse

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.