1 Descents, Eulerian numbers, and refined descent counts

This chapter formalizes Stanley EC1 §1.4 (descents and the Eulerian polynomials, pp. 30–51). The basic objects are: the descent set of a permutation, the Eulerian number \(A_{n+1,k+1}\) counting permutations of \([n+1]\) with exactly \(k\) descents, and the set-refined count \(\beta _n(S)\) giving the number of permutations whose descent set is exactly \(S\).

Throughout this chapter, indices shift by one between Stanley’s convention and ours: Stanley writes \(w \in \mathfrak {S}_n\) and \(D(w) \subseteq [n-1]\), while our formalization uses \(\sigma \in \mathfrak {S}_{n+1}\) and \(D(\sigma ) \subseteq \{ 0, \dots , n-1\} \) (modelled in MathComp by \(\texttt{\{ set 'I\_ n\} }\)). The mathematical content is identical.