Eulerian Numbers

This module formalizes the definition of Eulerian numbers (Section 6.2 from Concrete Mathematics).

The Eulerian number $\left\langle{n\atop k}\right\rangle$ counts the number of permutations of $\{1,2,\ldots,n\}$ with $k$ ascents.

References

• Concrete Mathematics

def eulerian (n k : ℕ) : ℕ

Equations

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

theorem eulerian_0_0 : eulerian 0 0 = 1

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

theorem eulerian_of_zero : eulerian 0 0 = 1

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

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

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

theorem smul_mul_eq {S : Type u_1} [NonAssocRing S] (r s : S) (a : ℕ) : a • r * s = r * a • s

theorem succ_mul_choose_eq {R : Type u_1} [NonAssocRing R] [Pow R ℕ] [BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ) : (n + 1) • Ring.choose (r + 1) (n + 1) = (r + 1) * Ring.choose r n