Hankel determinants of Eulerian polynomials

TheoremHankel determinants of the Eulerian polynomials#✓fully proved

For \(m \ge 0\) let \(P_m \in \mathbb{Z}[X]\) be the Eulerian polynomial \(P_m = \sum_{k=0}^{m} W_{m,k} X^k\), where \(W_{m,k} = \sum_{i=0}^{m-k} (-1)^i \binom{m+1}{i} (m-k-i)^m\) with \(0^0 = 1\) (so \(P_0 = 1\) and \(P_2 = 1 + X\)). Then for every \(n \ge 0\) the Hankel determinant \(\det(P_{i+j})_{0 \le i, j \le n}\) equals \(X^{\binom{n+1}{2}} \prod_{k=1}^{n} (k!)^2\).

The proof writes \(P_m\) as the moments of a weighted Motzkin table with down-step weights \(\lambda_k = k^2 X\) (Barry's Eulerian moment recurrence) and applies the weighted-Motzkin determinant theorem.

public theorem eulerianPolynomial_hankelDeterminant
    (P : ℕ → Polynomial ℤ)
    (hP : ∀ m : ℕ, P m =
      ∑ k ∈ Finset.range (m + 1),
        Polynomial.monomial k
          (∑ i ∈ Finset.range (m - k + 1),
            (-1 : ℤ) ^ i * (Nat.choose (m + 1) i : ℤ) *
              ((m - k - i : ℕ) : ℤ) ^ m))
    (n : ℕ) :
    Matrix.det (fun i j : Fin (n + 1) => P (i.val + j.val)) =
      Polynomial.X ^ Nat.choose (n + 1) 2 *
        Polynomial.C (∏ k ∈ Finset.range n, ((Nat.factorial (k + 1) : ℤ) ^ 2))
Sources
Uses 2

TheoremHankel determinants of the shifted Eulerian polynomials#✓fully proved

Let \(n \in \mathbb{N}\) and \(x \in \mathbb{R}\). For natural numbers \(k \le m\) let \(W_{m,k} = \sum_{i=0}^{m-k} (-1)^i \binom{m+1}{i} (m-k-i)^m\), with \(0^0 = 1\), and let \(P_m(X) = \sum_{k=0}^{m} W_{m,k} X^k\) be the corresponding Eulerian polynomial. Then the \((n+1) \times (n+1)\) Hankel determinant of the shifted sequence \(P_1(x), P_2(x), \dots\) is

\[\det\bigl(P_{i+j+1}(x)\bigr)_{0 \le i, j \le n} = (2x)^{\binom{n+1}{2}} \prod_{k=0}^{n-1} \binom{k+3}{2}^{n-k-1}.\]
public theorem hankel_transform_shifted_eulerian_polynomials :
  ∀ (n : ℕ) (x : ℝ) (W : ℕ → ℕ → ℝ) (P : ℕ → ℝ → ℝ),
    (∀ (m k : ℕ),
      W m k =
        ∑ i ∈ Finset.range (m - k + 1),
          (-1 : ℝ) ^ i * ((((m + 1).choose i : ℕ) : ℝ)) *
            (((((m - k - i : ℕ) : ℝ))) ^ m)) →
    (∀ (m : ℕ) (X : ℝ),
      P m X = ∑ k ∈ Finset.range (m + 1), W m k * X ^ k) →
    Matrix.det (Matrix.of fun (i j : Fin (n + 1)) => P (i.val + j.val + 1) x) =
      (2 * x) ^ ((n + 1).choose 2) *
        ∏ k ∈ Finset.range n,
          (((((k + 3).choose 2 : ℕ) : ℝ)) ^ (n - (k + 1)))
Sources
Uses 3
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.