Hankel transforms and Jacobi continued fractions

DefinitionHankel transform#✓fully proved

Let \(R\) be a commutative ring and let \((a_k)_{k \ge 0}\) be a sequence in \(R\). The Hankel transform of \(a\) is the sequence \((h_n)_{n \ge 0}\) in \(R\) whose term \(h_n\) is the determinant of the \((n + 1) \times (n + 1)\) Hankel matrix \((a_{i+j})_{0 \le i, j \le n}\).

def hankelTransform {R : Type*} [CommRing R] (a : ℕ → R) : ℕ → R :=
  fun n ↦ Matrix.det (Matrix.of fun i j : Fin (n + 1) ↦ a (i.val + j.val))
Used by 6
Used byHankel transforms of Jacobi fractions do not depend on the linear coefficients · Heilermann's formula · Heilermann's formula for weighted Motzkin arrays · Layman's theorem: the binomial transform preserves the Hankel transform · Hankel determinants of the Eulerian polynomials · Hankel determinants of the shifted Eulerian polynomials

DefinitionJacobi continued fraction expansion#✓fully proved

Let \(K\) be a ring, not necessarily commutative, let \((a_n)_{n \ge 0}\), \((\alpha_n)_{n \ge 0}\) and \((\beta_n)_{n \ge 0}\) be sequences in \(K\), let \(\mu_0 \in K\), and let \((F_i)_{i \ge 0}\) be a sequence of formal power series over \(K\) in the variable \(x\). These data form a Jacobi continued fraction expansion of \(a\) when \(\sum_{n \ge 0} a_n x^n = \mu_0 F_0\) and, for every \(i \ge 0\), \((1 - \alpha_i x - \beta_{i+1} x^2 F_{i+1}) F_i = 1\). Informally, the power series \(F_i\) are the tails of the continued fraction

\[ \sum_{n} a_n x^n = \cfrac{\mu_0}{1 - \alpha_0 x - \cfrac{\beta_1 x^2}{1 - \alpha_1 x - \cdots}}. \]

This records only the continued fraction identities, not Heilermann's formula for the Hankel determinants of \(a\).

def HasJacobiFraction {K : Type*} [Ring K] (a alpha beta : ℕ → K) (mu0 : K)
    (F : ℕ → PowerSeries K) : Prop :=
  PowerSeries.mk a = PowerSeries.C mu0 * F 0 ∧
    ∀ i : ℕ,
      (1 - PowerSeries.C (alpha i) * PowerSeries.X -
        PowerSeries.C (beta (i + 1)) * PowerSeries.X ^ 2 * F (i + 1)) * F i = 1
Sources
Used by 5
Used byMoment generating function as a J-fraction, general form · Moment generating function as a J-fraction · Weighted Motzkin recurrence for the coefficients of a Jacobi fraction · Hankel transforms of Jacobi fractions do not depend on the linear coefficients · Heilermann's formula
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.