Eulerian Numbers

This module defines the Eulerian numbers by their standard triangular recurrence (Section 6.2 of [Concrete Mathematics][knuth1989concrete]), proves their boundary values, and proves Worpitzky's identity (6.37): for all natural numbers x and n, x ^ n = ∑ k ∈ Finset.range (n + 1), eulerian n k * (x + k).choose n.

The combinatorial interpretation of $\left\langle{n\atop k}\right\rangle$ — counting the permutations of $\{1,2,\ldots,n\}$ with $k$ ascents — is not formalized here.

References

• [Concrete Mathematics][knuth1989concrete]

def SpecialNumbers.eulerian (n k : ℕ) : ℕ

Eulerian number, defined by the recurrence eulerian (n + 1) k = (k + 1) * eulerian n k + (n + 1 - k) * eulerian n (k - 1) with boundary values eulerian n 0 = 1 and eulerian 0 k = 0 for k > 0.

Equations

• SpecialNumbers.eulerian n 0 = 1
• SpecialNumbers.eulerian 0 k = 0
• SpecialNumbers.eulerian n_2.succ k = (k + 1) * SpecialNumbers.eulerian n_2 k + (n_2 + 1 - k) * SpecialNumbers.eulerian n_2 (k - 1)

theorem SpecialNumbers.eulerian_0_0 : eulerian 0 0 = 1

theorem SpecialNumbers.eulerian_of_n_zero (n : ℕ) : eulerian n 0 = 1

theorem SpecialNumbers.eulerian_of_zero : eulerian 0 0 = 1

theorem SpecialNumbers.eulerian_of_zero_k (k : ℕ) (h : k > 0) : eulerian 0 k = 0

theorem SpecialNumbers.eulerian_of_n_succ_n (n k : ℕ) (h : n > 0) (hp : k ≥ n) : eulerian n k = 0

theorem SpecialNumbers.eulerian_of_succ_n_n (n : ℕ) : eulerian (n + 1) n = 1

theorem SpecialNumbers.eulerian_eq_zero_of_lt {n k : ℕ} (h : n < k) : eulerian n k = 0

theorem SpecialNumbers.eulerian_succ_succ (n k : ℕ) : eulerian (n + 1) (k + 1) = (k + 1 + 1) * eulerian n (k + 1) + (n - k) * eulerian n k

theorem SpecialNumbers.worpitzky_step (x n k : ℕ) (hk : k ≤ n) : x * (x + k).choose n = (k + 1) * (x + k).choose (n + 1) + (n - k) * (x + k + 1).choose (n + 1)

The binomial-coefficient recurrence behind the inductive step of Worpitzky's identity: multiplying (x + k).choose n by x re-expands it in the basis of binomial coefficients of order n + 1. Valid over ℕ for k ≤ n.

theorem SpecialNumbers.sum_eulerian_succ_mul_choose (n x : ℕ) : ∑ k ∈ Finset.range (n + 1 + 1), eulerian (n + 1) k * (x + k).choose (n + 1) = ∑ k ∈ Finset.range (n + 1), (k + 1) * eulerian n k * (x + k).choose (n + 1) + ∑ k ∈ Finset.range (n + 1), (n - k) * eulerian n k * (x + k + 1).choose (n + 1)

Re-grouping step for Worpitzky's identity: the order-n + 1 Eulerian expansion arises from the order-n one via the triangular recurrence.

theorem SpecialNumbers.worpitzky (n x : ℕ) : x ^ n = ∑ k ∈ Finset.range (n + 1), eulerian n k * (x + k).choose n

Worpitzky's identity (Concrete Mathematics, identity (6.37)): the power x ^ n expands in the binomial-coefficient basis with Eulerian-number coefficients, x ^ n = ∑ k ∈ Finset.range (n + 1), eulerian n k * (x + k).choose n.