A- and Z-sequences of Riordan arrays

TheoremA- and Z-sequence characterization of integer Riordan arrays#✓fully proved

Let \((d_{n,k})_{n,k \ge 0}\) be an integer matrix that is lower triangular, that is, \(d_{n,k} = 0\) whenever \(n < k\). Then the following are equivalent: (i) there are power series \(g, f \in \mathbb{Z}[[x]]\) with \(g(0) = 1\), \(f(0) = 0\) and \([x^1]\, f \ne 0\) such that \(d_{n,k} = [x^n]\, g f^k\) for all \(n, k \ge 0\); (ii) \(d_{0,0} = 1\) and there are rational sequences \((A_j)_{j \ge 0}\) and \((Z_j)_{j \ge 0}\) with \(A_0 \ne 0\) such that, for all \(n, k \ge 0\),

\[d_{n+1,k+1} = \sum_{j=0}^{n} A_j\, d_{n,k+j} \quad\text{and}\quad d_{n+1,0} = \sum_{j=0}^{n} Z_j\, d_{n,j}.\]

The sequences are rational because \(A_0 = [x^1]\, f\) need not be a unit in \(\mathbb{Z}\).

Correction to the cited source: Barry's Proposition displays the hypothesis \(Z_0 \ne 0\), but the identity Riordan array has \(Z_0 = 0\), so that condition cannot hold in general. This statement therefore drops \(Z_0 \ne 0\) — a deliberate correction to the source, not just a normalization — and instead imposes the Riordan normalization \(d_{0,0} = 1\).

Proof: The forward implication uses coefficientwise triangular expansions in powers of \(f\); the converse reconstructs \(g\) and \(f\) from columns zero and one and proves rowwise uniqueness. This is the route of Barry's Proposition Char following He and Sprugnoli's Theorems 2.1 and 2.2.

public theorem riordan_iff_AZ_sequences (d : ℕ → ℕ → ℤ)
    (htri : ∀ n k : ℕ, n < k → d n k = 0) :
    ((∃ g f : PowerSeries ℤ, PowerSeries.constantCoeff (R := ℤ) g = 1 ∧
      PowerSeries.constantCoeff (R := ℤ) f = 0 ∧
      PowerSeries.coeff (R := ℤ) 1 f ≠ 0 ∧
      ∀ n k : ℕ, d n k = PowerSeries.coeff (R := ℤ) n (g * f ^ k)) ↔
    (∃ A Z : ℕ → ℚ, A 0 ≠ 0 ∧ d 0 0 = 1 ∧
      (∀ n k : ℕ, (d (n + 1) (k + 1) : ℚ) = ∑ j ∈ Finset.range (n + 1), A j * d n (k + j)) ∧
      (∀ n : ℕ, (d (n + 1) 0 : ℚ) = ∑ j ∈ Finset.range (n + 1), Z j * d n j)))
Sources

TheoremInverse of a Riordan array from its A- and Z-sequences (one-sided form)#✓fully proved

Let \(K\) be a field, let \(g, f, A, Z, \bar f\) be formal power series over \(K\), and let \(d_{00} \in K\) with \(d_{00} \ne 0\). Suppose that \(g(0) = d_{00}\), \(f(0) = 0\), \(A(0) \ne 0\), \(\bar f(0) = 0\), \(f(\bar f(x)) = x\), \(f(x) = x\, A(f(x))\) and \(g(x) = d_{00} \bigl(1 - x\, Z(f(x))\bigr)^{-1}\). Then

\[\left(\frac{1}{g(\bar f(x))},\ \bar f(x)\right) = \left(\frac{A(x) - x\, Z(x)}{d_{00}\, A(x)},\ \frac{x}{A(x)}\right).\]

Here \(A\) and \(Z\) are the generating functions of the A- and Z-sequences of the Riordan array \((g, f)\), and the pair on the left is its inverse. Only \(f(\bar f(x)) = x\) is assumed, not also \(\bar f(f(x)) = x\).

MetaMathlibExt.riordan_array_inverse_via_a_and_z_sequences_general · 17 lines 
theorem riordan_array_inverse_via_a_and_z_sequences_general
    {K : Type*} [Field K]
    (g f A Z fInv : PowerSeries K)
    (d₀₀ : K)
    (hd₀₀ : PowerSeries.constantCoeff g = d₀₀)
    (hd₀₀_ne : d₀₀ ≠ 0)
    (hf₀ : PowerSeries.constantCoeff f = 0)
    (hA₀ : PowerSeries.constantCoeff A ≠ 0)
    (hfInv₀ : PowerSeries.constantCoeff fInv = 0)
    (hA : f = (PowerSeries.X : PowerSeries K) * PowerSeries.subst f A)
    (hcomp_left : PowerSeries.subst fInv f = (PowerSeries.X : PowerSeries K))
    (hZ : g = PowerSeries.C (R := K) d₀₀ *
      ((1 - PowerSeries.X * PowerSeries.subst f Z : PowerSeries K)⁻¹)) :
    (((PowerSeries.subst fInv g)⁻¹, fInv) : PowerSeries K × PowerSeries K) =
      ((A - PowerSeries.X * Z) *
        ((PowerSeries.C (R := K) d₀₀ * A : PowerSeries K)⁻¹),
        (PowerSeries.X : PowerSeries K) * A⁻¹)
Used by 1
Used byInverse of a Riordan array from its A- and Z-sequences

TheoremInverse of a Riordan array from its A- and Z-sequences#✓fully proved

Let \(K\) be a field, let \(g, f, A, Z, \bar f\) be formal power series over \(K\), and let \(d_{00} \in K\) with \(d_{00} \ne 0\). Suppose that \(g(0) = d_{00}\), \(f(0) = 0\), \(A(0) \ne 0\) and \(\bar f(0) = 0\); that \(f(\bar f(x)) = x\) and \(\bar f(f(x)) = x\), so that \(\bar f\) is the compositional inverse of \(f\); that \(f(x) = x\, A(f(x))\), so that \(A\) is the generating function of the A-sequence; and that \(g(x) = d_{00} \bigl(1 - x\, Z(f(x))\bigr)^{-1}\), so that \(Z\) is the generating function of the Z-sequence. Then

\[\left(\frac{1}{g(\bar f(x))},\ \bar f(x)\right) = \left(\frac{A(x) - x\, Z(x)}{d_{00}\, A(x)},\ \frac{x}{A(x)}\right).\]

The pair on the left is the inverse of the Riordan array \((g, f)\). The hypothesis \(\bar f(f(x)) = x\) is not needed for the conclusion; it is kept to match the source.

MetaMathlibExt.riordan_array_inverse_via_a_and_z_sequences · 18 lines 
theorem riordan_array_inverse_via_a_and_z_sequences
  {K : Type*} [Field K]
  (g f A Z fInv : PowerSeries K)
  (d₀₀ : K)
  (hd₀₀ : PowerSeries.constantCoeff g = d₀₀)
  (hd₀₀_ne : d₀₀ ≠ 0)
  (hf₀ : PowerSeries.constantCoeff f = 0)
  (hA₀ : PowerSeries.constantCoeff A ≠ 0)
  (hfInv₀ : PowerSeries.constantCoeff fInv = 0)
  (hA : f = (PowerSeries.X : PowerSeries K) * PowerSeries.subst f A)
  (hcomp_left : PowerSeries.subst fInv f = (PowerSeries.X : PowerSeries K))
  (hcomp_right : PowerSeries.subst f fInv = (PowerSeries.X : PowerSeries K))
  (hZ : g = PowerSeries.C (R := K) d₀₀ *
    ((1 - PowerSeries.X * PowerSeries.subst f Z : PowerSeries K)⁻¹)) :
  (((PowerSeries.subst fInv g)⁻¹, fInv) : PowerSeries K × PowerSeries K) =
    ((A - PowerSeries.X * Z) *
      ((PowerSeries.C (R := K) d₀₀ * A : PowerSeries K)⁻¹),
      (PowerSeries.X : PowerSeries K) * A⁻¹)
Sources
Uses 1
Proof usesInverse of a Riordan array from its A- and Z-sequences (one-sided form)
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.