Peak descents of Dyck paths

DefinitionPeak descents#✓fully proved

Let \(l\) be a finite sequence of up steps \(U\) and down steps \(D\). A peak of \(l\) is a position where a step \(U\) is immediately followed by a step \(D\). The peak descents of \(l\) form the list that has, for each peak from left to right, the length \(j\) of the maximal run of consecutive steps \(D\) that starts at the \(D\) of that peak, so that the peak and its descent form the primitive block \(U D^j\).

def dyckPeakDescents (l : List DyckStep) : List ℕ :=
  ((List.range l.length).filter fun i => decide (l[i]? = some U ∧ l[i + 1]? = some D)).map
    fun i => ((l.drop (i + 1)).takeWhile (· == D)).length
Sources
  • Gil, Hoover, and Shearer, Bijections Between Colored Compositions, Dyck Paths, and Polygon Partitions, Journal of Integer Sequences 27 (2024), Article 24.5.2, Section 2 (Dyck paths).
Used by 3

TheoremPeak descents of a sample Dyck path#✓fully proved

The Dyck path \(UUUUDDDUDDUUDUUDDD\), which factors as \(U\,U\,U\,(UD^3)(UD^2)\,U\,(UD)\,U\,(UD^3)\), has four peaks \(UD\), and the lengths of the maximal runs of \(D\) steps starting at the \(D\) of each peak are, from left to right, \(3, 2, 1, 3\).

theorem dyckPeakDescents_sample :
    dyckPeakDescents [U, U, U, U, D, D, D, U, D, D, U, U, D, U, U, D, D, D] =
      [3, 2, 1, 3]
Sources
  • Gil, Hoover, and Shearer, Bijections Between Colored Compositions, Dyck Paths, and Polygon Partitions, Journal of Integer Sequences 27 (2024), Article 24.5.2, Section 2.
Uses 1
Statement usesPeak descents
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.