Generalized Catalan–Schröder numbers

TheoremFunctional equation of the generalized Catalan–Schröder recurrence#✓fully proved

Let \(R\) be a commutative ring, let \(s, t, p \in R\), and let \((a_n)_{n \ge 0}\) be a sequence in \(R\) with \(a_0 = 1\), \(a_1 = p\) and

\[a_n = s\,a_{n-1} + t \sum_{k=0}^{n-3} a_{k+1}\,a_{n-k-2} \qquad (n \ge 2).\]

Then the power series \(A = \sum_{n \ge 0} a_n X^n\) over \(R\) satisfies \(A - 1 = pX + sX\,(A - 1) + tX\,(A - 1)^2\).

public theorem generalizedCatalanSchroeder_recurrence_functionalEquation
    (R : Type) [CommRing R] (s t p : R) (a : ℕ → R) (ha0 : a 0 = 1) (ha1 : a 1 = p)
    (hrec : ∀ n : ℕ, 2 ≤ n →
      a n = s * a (n - 1) +
        t * Finset.sum (Finset.range (n - 2)) (fun k => a (k + 1) * a (n - k - 2))) :
    PowerSeries.mk a - 1 =
      PowerSeries.C p * PowerSeries.X +
        PowerSeries.C s * PowerSeries.X * (PowerSeries.mk a - 1) +
          PowerSeries.C t * PowerSeries.X * (PowerSeries.mk a - 1) ^ 2
Used by 1
Used byGenerating function of the generalized Catalan–Schröder numbers

TheoremGenerating function of the generalized Catalan–Schröder numbers#✓fully proved

Let \(R\) be a commutative ring, let \(s, t, p \in R\), and let \((a_n)_{n \ge 0}\) be a sequence in \(R\) with \(a_0 = 1\), \(a_1 = p\) and

\[a_n = s\,a_{n-1} + t \sum_{k=0}^{n-3} a_{k+1}\,a_{n-k-2} \qquad (n \ge 2).\]

Let \(g\) and \(f\) be formal power series over \(R\) with

\[(1 - (s - 2t)X)\,g = 1 + (p - s + t)X, \qquad (1 - (s - 2t)X)^2 f = tX\,(1 + (p - s + t)X),\]

and let \(C(X) = \sum_{n \ge 0} C_n X^n\), where \(C_n\) is the \(n\)-th Catalan number viewed in \(R\). Then \(\sum_{n \ge 0} a_n X^n = g \cdot C(f)\), where \(C(f)\) is the power series obtained by substituting \(f\) for \(X\) in \(C\). Since \(1 - (s - 2t)X\) is invertible in \(R[[X]]\), these equations determine \(g\) and \(f\), and \(f\) has zero constant term.

Barry prints \(f\) without the factor \(X\) in \(1 + (p - s + t)X\). That version is false: for \(s = 2\), \(t = 1\), \(p = 2\) the resulting series \(g \cdot C(f)\) has coefficient \(3\) at \(X\), not \(a_1 = 2\). The recurrence forces the factor restored here.

The proof substitutes \(f\) into the Catalan equation \(C = 1 + X C^2\), shows that \(g \cdot C(f)\) satisfies the same quadratic functional equation as \(\sum_{n \ge 0} a_n X^n\), and concludes by comparing coefficients.

public theorem generalizedCatalanSchroeder_generatingFunction (R : Type) [CommRing R]
    (s : R) (t : R) (p : R) (a : ℕ → R) (ha0 : a 0 = 1) (ha1 : a 1 = p)
    (hrec : ∀ n : ℕ, 2 ≤ n →
      a n = s * a (n - 1) +
        t * Finset.sum (Finset.range (n - 2)) (fun k => a (k + 1) * a (n - k - 2)))
    (g : PowerSeries R)
    (hg : (1 - PowerSeries.C (s - 2 * t) * PowerSeries.X) * g =
      1 + PowerSeries.C (p - s + t) * PowerSeries.X)
    (f : PowerSeries R)
    (hf : (1 - PowerSeries.C (s - 2 * t) * PowerSeries.X) ^ 2 * f =
      PowerSeries.C t * PowerSeries.X * (1 + PowerSeries.C (p - s + t) * PowerSeries.X)) :
    PowerSeries.mk a = g * PowerSeries.subst f (PowerSeries.mk (fun n => (catalan n : R)))
Sources
Uses 1
Proof usesFunctional equation of the generalized Catalan–Schröder recurrence
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.