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).
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]
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
MathlibExt/Combinatorics/Enumerative/DyckPeakDescents.lean:36
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.