Sequence transforms and generating functions

Operators on integer sequences and coefficient extraction: binomial, multiple and falling k-binomial transforms, INVERT and Catalan transforms, hypersequences, convolutions, C-finite sequences, and recovering terms from generating-function values.

TheoremBarry's Catalan transform and its inverse#✓fully proved

Let \(a, b \colon \mathbb{N} \to \mathbb{Q}\) be sequences such that, for every \(n \ge 0\),

\[b_n = \sum_{j=0}^{n} \sum_{k=0}^{n} \frac{2k+1}{n+k+1} (-1)^{k-j} \binom{2n}{n-k} \binom{k}{j} a_j.\]

Then for every \(n \ge 1\) both

\[b_n = \sum_{k=0}^{n} \frac{k}{2n-k} \binom{2n-k}{n-k} a_k\]

and

\[b_n = \sum_{k=0}^{n} \frac{k}{n} \binom{2n-k-1}{n-k} a_k\]

hold, and for every \(n \ge 0\) both

\[a_n = \sum_{k=0}^{\lfloor n/2 \rfloor} (-1)^k \binom{n-k}{k} b_{n-k}\]

and

\[a_n = \sum_{k=0}^{n} (-1)^{n-k} \binom{k}{n-k} b_k\]

hold.

In the hypothesis, the terms with \(j > k\) vanish because \(\binom{k}{j} = 0\) there.

theorem catalan_transform_pair (a b : ℕ → ℚ)
    (h : ∀ n, b n = ∑ j ∈ Finset.range (n + 1), ∑ k ∈ Finset.range (n + 1),
      ((2 * (k : ℚ) + 1) / ((n : ℚ) + (k : ℚ) + 1)) * (-1 : ℚ) ^ (k - j) *
        (Nat.choose (2 * n) (n - k) : ℚ) * (Nat.choose k j : ℚ) * a j) :
    (∀ n, 0 < n → b n = ∑ k ∈ Finset.range (n + 1),
      ((k : ℚ) / (2 * (n : ℚ) - (k : ℚ))) * (Nat.choose (2 * n - k) (n - k) : ℚ) * a k) ∧
    (∀ n, 0 < n → b n = ∑ k ∈ Finset.range (n + 1),
      ((k : ℚ) / (n : ℚ)) * (Nat.choose (2 * n - k - 1) (n - k) : ℚ) * a k) ∧
    (∀ n, a n = ∑ k ∈ Finset.range (n / 2 + 1),
      (Nat.choose (n - k) k : ℚ) * (-1 : ℚ) ^ k * b (n - k)) ∧
    (∀ n, a n = ∑ k ∈ Finset.range (n + 1),
      (Nat.choose k (n - k) : ℚ) * (-1 : ℚ) ^ (n - k) * b k)
Sources

DefinitionC-finite polynomial sequences#✓fully proved

Let \(\sigma\) be a type indexing variables, and write \(\mathbb{Z}[\sigma]\) for the multivariate polynomials with integer coefficients in the variables \(\sigma\). A sequence \(a_0, a_1, a_2, \dots\) in \(\mathbb{Z}[\sigma]\) is C-finite when there exist natural numbers \(k\) and \(N\) and polynomials \(p_1, \dots, p_k \in \mathbb{Z}[\sigma]\) such that for every \(n \ge N\)

\[ a_{n+k+1} = \sum_{i=1}^{k} p_i \, a_{n+i}. \]
def IsCFiniteSequence {σ : Type*} (a : ℕ → MvPolynomial σ ℤ) : Prop :=
  ∃ (k N : ℕ) (c : Fin k → MvPolynomial σ ℤ),
    ∀ n ≥ N, a (n + k + 1) = ∑ i : Fin k, c i * a (n + i.val + 1)

TheoremHadamard product of two Fibonacci-type series#✓fully proved

Let \(R\) be a commutative ring, let \(a, b \in R\), and let \(n \ge 2\) be a natural number. For each \(k\), let \(f_k\) be the coefficient of \(x^k\) in \(1/(1 - ax - x^2)\) and \(g_k\) the coefficient of \(x^k\) in \(1/(1 - bx - x^n)\), the inverses taken in \(R[[x]]\). Then the Hadamard product \(\sum_{k \ge 0} f_k g_k x^k\) equals

\[ \frac{1 - f_{n-2}\, x^n}{1 - ab\, x - b^2 x^2 - (f_n + f_{n-2})\, x^n - (2b f_{n-1} - ab f_{n-2})\, x^{n+1} + (-1)^n x^{2n}} \]

in \(R[[x]]\), where the denominator has constant coefficient \(1\) and so is invertible.

MetaMathlibExt.hadamard_fibonacci_product · 17 lines 
theorem hadamard_fibonacci_product (R : Type _) [CommRing R] (a b : R)
    (n : ℕ) (hn : 2 ≤ n) :
  let f := fun k =>
    PowerSeries.coeff k
      (PowerSeries.invOfUnit
        (1 - PowerSeries.C a * PowerSeries.X - PowerSeries.X ^ 2) (1 : Rˣ))
  PowerSeries.mk (fun k =>
      f k * PowerSeries.coeff k
        (PowerSeries.invOfUnit
          (1 - PowerSeries.C b * PowerSeries.X - PowerSeries.X ^ n) (1 : Rˣ))) =
    (1 - PowerSeries.C (f (n - 2)) * PowerSeries.X ^ n) *
      PowerSeries.invOfUnit
        (1 - PowerSeries.C (a * b) * PowerSeries.X - PowerSeries.C (b ^ 2) * PowerSeries.X ^ 2 -
          PowerSeries.C (f n + f (n - 2)) * PowerSeries.X ^ n -
          PowerSeries.C (2 * b * f (n - 1) - a * b * f (n - 2)) * PowerSeries.X ^ (n + 1) +
          PowerSeries.C ((-1 : R) ^ n) * PowerSeries.X ^ (2 * n))
        (1 : Rˣ)
Sources

TheoremRecovering a sequence term from its generating function#✓fully proved

Let \(t_0, t_1, t_2, \dots\) be natural numbers and let \(c\), \(m\), \(N\) be natural numbers with \(c \ge 2\) and \(2 \le m \le N\). Suppose that the real series \(\sum_{k \ge 0} t_k \, (c^{-N})^k\) is summable and that \(t_j < c^{j-2}\) for every \(j \ge m\). Then

\[t_N = \Bigl\lfloor c^{N^2} \sum_{k \ge 0} t_k \, (c^{-N})^k \Bigr\rfloor \bmod c^N.\]
theorem generating_function_term_extraction
    (t : ℕ → ℕ) (c m N : ℕ)
    (hc : 2 ≤ c) (hm : 2 ≤ m) (hmN : m ≤ N)
    (hconv : Summable (fun k : ℕ => (t k : ℝ) * (((c : ℝ) ^ N)⁻¹) ^ k))
    (hbound : ∀ j, m ≤ j → t j < c ^ (j - 2)) :
    t N = Nat.floor ((c : ℝ) ^ (N ^ 2) *
      (∑' k : ℕ, (t k : ℝ) * (((c : ℝ) ^ N)⁻¹) ^ k)) % c ^ N
Sources
  • M. Prunescu and J. M. Shunia, "On Modular Representations of C-Recursive Integer Sequences", Journal of Integer Sequences 28 (2025), Article 25.5.3, Theorem ThmExtraction1, source lines 169–173, https://cs.uwaterloo.ca/journals/JIS/VOL28/Prunescu/prunescu3.tex. The paper attributes the result to Prunescu and Sauras-Altuzarra. Only the first representation (for N ≥ m ≥ 2 with t j < c ^ (j - 2)) is recorded, not the c ≥ 8 variant for all n ≥ 1.
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.