Heilermann's formula

TheoremHeilermann's formula#✓fully proved

Let \(K\) be a commutative ring, let \(a\), \(\alpha\), \(\beta\) be sequences in \(K\) and let \(\mu_0 \in K\). Suppose that \(a\) has Jacobi fraction data \((\alpha, \beta, \mu_0)\): there are power series \(F_0, F_1, \dots\) over \(K\) with \(\sum_{n \ge 0} a_n x^n = \mu_0 F_0\) and \((1 - \alpha_i x - \beta_{i+1} x^2 F_{i+1}) F_i = 1\) for every \(i \ge 0\). Then for every \(n \ge 0\) the Hankel transform of \(a\) at \(n\), the determinant of the \((n+1) \times (n+1)\) matrix \((a_{i+j})_{0 \le i, j \le n}\), equals

\[\mu_0^{n+1} \prod_{j=0}^{n-1} \beta_{j+1}^{\,n-j},\]

that is, \(\mu_0^{n+1} \beta_1^n \beta_2^{n-1} \cdots \beta_n\), which is \(\mu_0\) for \(n = 0\).

theorem hankelTransform_eq_prod_of_hasJacobiFraction
    {a alpha beta : ℕ → K} {mu0 : K} {F : ℕ → PowerSeries K}
    (h : HasJacobiFraction a alpha beta mu0 F) (n : ℕ) :
    hankelTransform a n =
      mu0 ^ (n + 1) * ∏ j ∈ Finset.range n, beta (j + 1) ^ (n - j)
Sources
  • Paul Barry, "From Fibonacci to Robbins: Series Reversion and Hankel Transforms," Journal of Integer Sequences 24 (2021), Article 21.10.2, https://cs.uwaterloo.ca/journals/JIS/VOL24/Barry2/barry461.tex, lines 110-117. Zero-indexed: hankelTransform a n is the determinant of the (n + 1) x (n + 1) Hankel matrix, and the product over Finset.range n with shift beta (j + 1) and exponent n - j gives beta_1 ^ n, ..., beta_n ^ 1; for n = 0 the empty product yields mu0. Scope: only the determinant identity is stated; the Jacobi continued fraction data itself is carried by HasJacobiFraction.
Uses 2 · Used by 1
Statement usesJacobi continued fraction expansion · Hankel transform
Used byHankel transforms of Jacobi fractions do not depend on the linear coefficients

TheoremHankel transforms of Jacobi fractions do not depend on the linear coefficients#✓fully proved

Let \(K\) be a commutative ring. Say that a sequence \(a\) in \(K\) has Jacobi fraction data \((\alpha, \beta, \mu_0)\), where \(\alpha\), \(\beta\) are sequences in \(K\) and \(\mu_0 \in K\), when there are power series \(F_0, F_1, \dots\) over \(K\) with \(\sum_{n \ge 0} a_n x^n = \mu_0 F_0\) and \((1 - \alpha_i x - \beta_{i+1} x^2 F_{i+1}) F_i = 1\) for every \(i \ge 0\). If \(a\) has Jacobi fraction data \((\alpha, \beta, \mu_0)\) and \(a'\) has Jacobi fraction data \((\alpha', \beta, \mu_0)\), with the same \(\beta\) and \(\mu_0\) but arbitrary \(\alpha\) and \(\alpha'\), then \(a\) and \(a'\) have the same Hankel transform: for every \(n \ge 0\) the determinants of the \((n+1) \times (n+1)\) matrices \((a_{i+j})_{0 \le i, j \le n}\) and \((a'_{i+j})_{0 \le i, j \le n}\) are equal.

theorem hankelTransform_eq_of_hasJacobiFraction_same_beta
    (a a2 alpha alpha2 beta : ℕ → K) (mu0 : K)
    (F F2 : ℕ → PowerSeries K)
    (h1 : HasJacobiFraction a alpha beta mu0 F)
    (h2 : HasJacobiFraction a2 alpha2 beta mu0 F2) :
    hankelTransform a = hankelTransform a2
Sources
Uses 3
Statement usesJacobi continued fraction expansion · Hankel transform
Proof usesHeilermann's formula

TheoremWeighted Motzkin recurrence for the coefficients of a Jacobi fraction#✓fully proved

Let \(K\) be a ring, let \(a\), \(\alpha\), \(\beta\) be sequences in \(K\) and let \(\mu_0 \in K\). Suppose that \(a\) has Jacobi fraction data \((\alpha, \beta, \mu_0)\): there are power series \(F_0, F_1, \dots\) over \(K\) with \(\sum_{n \ge 0} a_n x^n = \mu_0 F_0\) and \((1 - \alpha_i x - \beta_{i+1} x^2 F_{i+1}) F_i = 1\) for every \(i \ge 0\). Then there is an array \((M_{n,j})_{n, j \ge 0}\) in \(K\) with \(M_{0,0} = 1\) and, for all \(n, j \ge 0\), \(M_{0,j+1} = 0\), \(M_{n+1,0} = \alpha_0 M_{n,0} + \beta_1 M_{n,1}\) and \(M_{n+1,j+1} = M_{n,j} + \alpha_{j+1} M_{n,j+1} + \beta_{j+2} M_{n,j+2}\), such that \(a_n = \mu_0 M_{n,0}\) for every \(n \ge 0\).

theorem exists_weightedMotzkin_coefficients_of_hasJacobiFraction
    {K : Type*} [Ring K]
    {a alpha beta : ℕ → K} {mu0 : K} {F : ℕ → PowerSeries K}
    (h : HasJacobiFraction a alpha beta mu0 F) :
    ∃ M : ℕ → ℕ → K, M 0 0 = 1 ∧
      (∀ j, M 0 (j + 1) = 0) ∧
      (∀ n, M (n + 1) 0 = alpha 0 * M n 0 + beta 1 * M n 1) ∧
      (∀ n j, M (n + 1) (j + 1) =
        M n j + alpha (j + 1) * M n (j + 1) +
          beta (j + 2) * M n (j + 2)) ∧
      ∀ n, a n = mu0 * M n 0
Sources
  • Paul Barry, From Fibonacci to Robbins: Series Reversion and Hankel Transforms, Journal of Integer Sequences 24 (2021), Article 21.10.2, lines 110–117, https://cs.uwaterloo.ca/journals/JIS/VOL24/Barry2/barry461.tex. Barry does not explicitly state this auxiliary tableau lemma; it is a coefficientwise bridge for the displayed fraction.
Uses 1
Statement usesJacobi continued fraction expansion

TheoremHeilermann's formula for weighted Motzkin arrays#✓fully proved

Let \(K\) be a commutative ring, let \(\alpha\), \(\beta\) be sequences in \(K\), let \(\mu_0 \in K\), and let \((M_{n,j})_{n, j \ge 0}\) be an array in \(K\) with \(M_{0,0} = \mu_0\) and, for all \(n, j \ge 0\), \(M_{0,j+1} = 0\), \(M_{n+1,0} = \alpha_0 M_{n,0} + \beta_1 M_{n,1}\) and \(M_{n+1,j+1} = M_{n,j} + \alpha_{j+1} M_{n,j+1} + \beta_{j+2} M_{n,j+2}\). Then for every \(n \ge 0\) the Hankel transform of the column \((M_{m,0})_{m \ge 0}\) at \(n\), the determinant of the \((n+1) \times (n+1)\) matrix \((M_{i+j,0})_{0 \le i, j \le n}\), equals

\[\mu_0^{n+1} \prod_{j=0}^{n-1} \beta_{j+1}^{\,n-j},\]

that is, \(\mu_0^{n+1} \beta_1^n \beta_2^{n-1} \cdots \beta_n\), which is \(\mu_0\) for \(n = 0\).

No hypothesis that the \(\beta_i\) are nonzero is needed.

theorem hankelTransform_eq_prod_of_weightedMotzkin
    {K : Type*} [CommRing K]
    {alpha beta : ℕ → K} {M : ℕ → ℕ → K} {mu0 : K}
    (hzero : M 0 0 = mu0)
    (hzero_succ : ∀ j : ℕ, M 0 (j + 1) = 0)
    (hbase : ∀ n : ℕ, M (n + 1) 0 = alpha 0 * M n 0 + beta 1 * M n 1)
    (hstep : ∀ n j : ℕ, M (n + 1) (j + 1) =
      M n j + alpha (j + 1) * M n (j + 1) + beta (j + 2) * M n (j + 2))
    (n : ℕ) :
    hankelTransform (fun m => M m 0) n =
      mu0 ^ (n + 1) * ∏ j ∈ Finset.range n, beta (j + 1) ^ (n - j)
Sources
  • Paul Barry, From Fibonacci to Robbins: Series Reversion and Hankel Transforms, Journal of Integer Sequences 24 (2021), Article 21.10.2, lines 110–117, https://cs.uwaterloo.ca/journals/JIS/VOL24/Barry2/barry461.tex.
Uses 1 · Used by 2
Statement usesHankel transform
Used byHankel determinants of the Eulerian polynomials · Hankel determinants of the shifted Eulerian polynomials
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.