Eulerian numbers of multiset permutations

DefinitionDescent number of a word#✓fully proved

For a word \(w = w_1 \cdots w_K\) of length \(K\) over the alphabet \(\{0, 1, \dots, m-1\}\), the descent number of \(w\) is one more than its number of descents: \(1 + \#\{j : 1 \le j < K,\ w_j > w_{j+1}\}\).

The extra \(1\) follows the source convention, which also counts a descent at the end of the word; in particular the empty word has descent number \(1\).

def multisetDescentNumber {m K : ℕ} (w : Fin K → Fin m) : ℕ :=
  ((Finset.range K).filter fun j =>
    if h : j + 1 < K then w ⟨j, Nat.lt_of_succ_lt h⟩ > w ⟨j + 1, h⟩ else False).card + 1

Used by 1

Used byEulerian numbers of multiset permutations

DefinitionMultiset permutation#✓fully proved

Let \(k_0, \dots, k_{m-1}\) be natural numbers. A word \(w = w_1 \cdots w_K\) of length \(K\) over the alphabet \(\{0, 1, \dots, m-1\}\) is a permutation of the multiset with \(k_i\) copies of each letter \(i\) when, for every letter \(i\), exactly \(k_i\) positions \(j\) have \(w_j = i\).

def IsMultisetPermutation {m K : ℕ} (k : Fin m → ℕ) (w : Fin K → Fin m) : Prop :=
  ∀ i, ((Finset.univ : Finset (Fin K)).filter fun j => w j = i).card = k i

Used by 1

Used byEulerian numbers of multiset permutations

DefinitionEulerian numbers of multiset permutations#✓fully proved

Let \(k_0, \dots, k_{m-1}\) be natural numbers with sum \(K\), and let \(p\) be a natural number. The multiset Eulerian number is the number of words of length \(K\) over the alphabet \(\{0, 1, \dots, m-1\}\) that are permutations of the multiset with \(k_i\) copies of each letter \(i\) and whose descent number, one more than the number of descents, equals \(p\).

For multiplicities \(2, 2\), its nonzero values are \(1, 4, 1\) at \(p = 1, 2, 3\).

def multisetEulerianNumber {m : ℕ} (k : Fin m → ℕ) (p : ℕ) : ℕ :=
  let K := Finset.sum Finset.univ k
  ((Finset.univ : Finset (Fin K → Fin m)).filter fun w =>
    IsMultisetPermutation k w ∧ multisetDescentNumber w = p).card

def IsMultisetPermutation {m K : ℕ} (k : Fin m → ℕ) (w : Fin K → Fin m) : Prop :=
  ∀ i, ((Finset.univ : Finset (Fin K)).filter fun j => w j = i).card = k i

MathlibExt/Combinatorics/Enumerative/MultisetEulerianNumber.lean:34

def multisetDescentNumber {m K : ℕ} (w : Fin K → Fin m) : ℕ :=
  ((Finset.range K).filter fun j =>
    if h : j + 1 < K then w ⟨j, Nat.lt_of_succ_lt h⟩ > w ⟨j + 1, h⟩ else False).card + 1

MathlibExt/Combinatorics/Enumerative/MultisetEulerianNumber.lean:28

Uses 2

Statement usesMultiset permutation · Descent number of a word

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.