INVERT transform

TheoremLinear recurrence for INVERT convolution powers in characteristic zero#✓fully proved

Let \(K\) be a field of characteristic zero and let \((c_m)_{m \ge 0}\) and \((y_n)_{n \ge 0}\) be sequences in \(K\) such that for every \(n \ge 0\)

\[y_n = \sum_{k=0}^{n} k! \sum_{j} \prod_{i=1}^{n+1} \frac{c_i^{j_i}}{j_i!},\]

where the inner sum runs over all tuples \((j_1, \dots, j_{n+1})\) of integers with \(0 \le j_i \le n\), \(j_1 + j_2 + \dots + j_{n+1} = k\) and \(j_1 + 2 j_2 + \dots + (n+1) j_{n+1} = n\). Let \(r \ge 1\) be an integer, and for \(N \ge 0\) let \(y^{(r)}_N\) be the sum of \(y_{a_1} y_{a_2} \cdots y_{a_r}\) over all tuples \((a_1, \dots, a_r)\) of nonnegative integers with \(a_1 + \dots + a_r = N\). Then for every \(n \ge 1\)

\[n \, y^{(r)}_n = \sum_{m=1}^{n} \bigl(n + m(r-1)\bigr) \, c_m \, y^{(r)}_{n-m}.\]

The hypothesis says that \(y_n = \sum_{k=0}^{n} \frac{k!}{n!} B_{n,k}(1!\,c_1, 2!\,c_2, \dots)\) with the partial Bell polynomials \(B_{n,k}\), that is, \(y\) is the INVERT transform of \(c\): as formal power series in \(z\), \(\sum_{n \ge 0} y_n z^n = 1/(1 - \sum_{m \ge 1} c_m z^m)\). The value \(c_0\) plays no role, and the theorem for real sequences is the case \(K = \mathbb{R}\).

theorem bell_convolution_linear_recurrence_of_charZero (c : ℕ → K) (y : ℕ → K)
    (r : ℕ) (hr : 0 < r)
    (hBell : ∀ n : ℕ, y n = ∑ k ∈ Finset.range (n + 1), (k.factorial : K) *
      ∑ j ∈ (Fintype.piFinset (fun _ : Fin (n + 1) => Finset.range (n + 1))).filter
        (fun j => (∑ i, j i = k) ∧ (∑ i, (i.val + 1) * j i = n)),
      ∏ i, ((c (i.val + 1)) ^ (j i) / (((j i).factorial : ℕ) : K)))
    (n : ℕ) (hn : 1 ≤ n) :
    let conv : ℕ → K := fun N =>
      ∑ f ∈ Finset.univ.filter
        (fun f : Fin r → Fin (N + 1) => ∑ i, (f i).val = N),
      ∏ i, y ((f i).val);
    (n : K) * conv n = ∑ m ∈ Finset.Icc 1 n, ((n + m * (r - 1) : ℕ) : K) * c m * conv (n - m)

Used by 2

Used byLinear recurrence for convolution powers of an INVERT sequence · Linear recurrence for INVERT convolution powers via partial Bell polynomials

TheoremLinear recurrence for convolution powers of an INVERT sequence#✓fully proved

Let \((c_m)_{m \ge 0}\) and \((y_n)_{n \ge 0}\) be real sequences such that for every \(n \ge 0\)

\[y_n = \sum_{k=0}^{n} k! \sum_{j} \prod_{i=1}^{n+1} \frac{c_i^{j_i}}{j_i!},\]

where the inner sum runs over all tuples \((j_1, \dots, j_{n+1})\) of integers with \(0 \le j_i \le n\), \(j_1 + j_2 + \dots + j_{n+1} = k\) and \(j_1 + 2 j_2 + \dots + (n+1) j_{n+1} = n\). Let \(r \ge 1\) be an integer, and for \(N \ge 0\) let \(y^{(r)}_N\) be the sum of \(y_{a_1} y_{a_2} \cdots y_{a_r}\) over all tuples \((a_1, \dots, a_r)\) of nonnegative integers with \(a_1 + \dots + a_r = N\). Then for every \(n \ge 1\)

\[n \, y^{(r)}_n = \sum_{m=1}^{n} \bigl(n + m(r-1)\bigr) \, c_m \, y^{(r)}_{n-m}.\]

The hypothesis says that \(y_n = \sum_{k=0}^{n} \frac{k!}{n!} B_{n,k}(1!\,c_1, 2!\,c_2, \dots)\) with the partial Bell polynomials \(B_{n,k}\), that is, \(y\) is the INVERT transform of \(c\): as formal power series in \(z\), \(\sum_{n \ge 0} y_n z^n = 1/(1 - \sum_{m \ge 1} c_m z^m)\). The value \(c_0\) plays no role.

theorem bell_convolution_linear_recurrence (c : ℕ → ℝ) (y : ℕ → ℝ)
    (r : ℕ) (hr : 0 < r)
    (hBell : ∀ n : ℕ, y n = ∑ k ∈ Finset.range (n + 1), (k.factorial : ℝ) *
      ∑ j ∈ (Fintype.piFinset (fun _ : Fin (n + 1) => Finset.range (n + 1))).filter
        (fun j => (∑ i, j i = k) ∧ (∑ i, (i.val + 1) * j i = n)),
      ∏ i, ((c (i.val + 1)) ^ (j i) / (((j i).factorial : ℕ) : ℝ)))
    (n : ℕ) (hn : 1 ≤ n) :
    let conv : ℕ → ℝ := fun N =>
      ∑ f ∈ Finset.univ.filter
        (fun f : Fin r → Fin (N + 1) => ∑ i, (f i).val = N),
      ∏ i, y ((f i).val);
    (n : ℝ) * conv n = ∑ m ∈ Finset.Icc 1 n, ((n + m * (r - 1) : ℕ) : ℝ) * c m * conv (n - m)

Sources

• Daniel Birmajer, Juan B. Gil, and Michael D. Weiner, "Linear Recurrence Sequences and Their Convolutions via Bell Polynomials," Journal of Integer Sequences 18 (2015), Article 15.1.2, Theorem, equation, lines 425–435, https://cs.uwaterloo.ca/journals/JIS/VOL18/Gil/gil3.tex

Uses 1

Proof usesLinear recurrence for INVERT convolution powers in characteristic zero

TheoremLinear recurrence for INVERT convolution powers via partial Bell polynomials#✓fully proved

Let \(K\) be a field of characteristic zero, let \((c_m)_{m \ge 0}\) and \((y_n)_{n \ge 0}\) be sequences in \(K\), and write \(B_{n,k}\) for the partial Bell polynomial. Suppose that for every \(n \ge 0\)

\[y_n = \sum_{k=0}^{n} \frac{k!}{n!} \, B_{n,k}(x_1, x_2, \dots), \qquad x_m = m! \, c_m.\]

Let \(r \ge 1\) be an integer, and for \(N \ge 0\) let \(y^{(r)}_N\) be the sum of \(y_{a_1} y_{a_2} \cdots y_{a_r}\) over all tuples \((a_1, \dots, a_r)\) of nonnegative integers with \(a_1 + \dots + a_r = N\). Then for every \(n \ge 1\)

\[n \, y^{(r)}_n = \sum_{m=1}^{n} \bigl(n + m(r-1)\bigr) \, c_m \, y^{(r)}_{n-m}.\]

theorem bell_convolution_linear_recurrence_partialBellPolynomial (c : ℕ → K) (y : ℕ → K)
    (r : ℕ) (hr : 0 < r)
    (hBell : ∀ n : ℕ, y n = ∑ k ∈ Finset.range (n + 1), (k.factorial : K) / n.factorial *
      partialBellPolynomial n k (fun m => (m.factorial : K) * c m))
    (n : ℕ) (hn : 1 ≤ n) :
    let conv : ℕ → K := fun N =>
      ∑ f ∈ Finset.univ.filter
        (fun f : Fin r → Fin (N + 1) => ∑ i, (f i).val = N),
      ∏ i, y ((f i).val);
    (n : K) * conv n = ∑ m ∈ Finset.Icc 1 n, ((n + m * (r - 1) : ℕ) : K) * c m * conv (n - m)

Uses 2

Statement usesPartial Bell polynomial

Proof usesLinear recurrence for INVERT convolution powers in characteristic zero

DefinitionThe INVERT transform of an integer sequence#✓fully proved

The INVERT transform of an integer sequence \(a = (a_n)_{n \ge 0}\) is the integer sequence \(b = (b_n)_{n \ge 0}\) in which \(b_n\) is the coefficient of \(x^{n+1}\) in the inverse of \(1 - \sum_{m \ge 0} a_m x^{m+1}\) in \(\mathbb{Z}[[x]]\) (the inverse exists because the constant coefficient is \(1\)). In the one-based indexing of the source, \(a_n\) and \(b_n\) are the terms of index \(n + 1\).

noncomputable def invertTransform (a : ℕ → ℤ) : ℕ → ℤ :=
  fun n => PowerSeries.coeff (n + 1) ((1 - PowerSeries.X * PowerSeries.mk a).invOfUnit 1)

Used by 1

Used byGenerating function of the INVERT transform

TheoremGenerating function of the INVERT transform#✓fully proved

Let \(a = (a_n)_{n \ge 0}\) be an integer sequence and \(b = (b_n)_{n \ge 0}\) its INVERT transform, and put \(A(x) = \sum_{n \ge 0} a_n x^{n+1}\) and \(B(x) = \sum_{n \ge 0} b_n x^{n+1}\). Then \((1 - A(x))(1 + B(x)) = 1\) in \(\mathbb{Z}[[x]]\), that is, \(1 + B(x)\) is the inverse of \(1 - A(x)\).

theorem invertTransform_spec (a : ℕ → ℤ) :
    (1 - PowerSeries.X * PowerSeries.mk a) *
      (1 + PowerSeries.X * PowerSeries.mk (invertTransform a)) = 1

Uses 1

Statement usesThe INVERT transform of an integer sequence

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.