Commit 2024-08-23 17:13 6e23e475

View on Github →

feat: first return of a Dyck word (#15864) Second part of #9781. This also includes a PartialOrder instance on Dyck words directly reflecting the tree bijection, that in turn allows a positivity extension for firstReturn.

Estimated changes

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

modified theorem DyckWord.cons_tail_dropLast_concat

added theorem DyckWord.count_D_lt_count_U_of_lt_firstReturn

added theorem DyckWord.count_take_firstReturn_add_one

modified def DyckWord.denest

modified theorem DyckWord.denest_nest

added def DyckWord.firstReturn

added theorem DyckWord.firstReturn_add

added theorem DyckWord.firstReturn_lt_length

added theorem DyckWord.firstReturn_nest

added theorem DyckWord.firstReturn_nest_add

added theorem DyckWord.firstReturn_pos

added theorem DyckWord.firstReturn_zero

modified theorem DyckWord.getLast_eq_D

modified theorem DyckWord.head_eq_U

added theorem DyckWord.infix_of_le

added def DyckWord.insidePart

added theorem DyckWord.insidePart_nest_add

added theorem DyckWord.insidePart_zero

added theorem DyckWord.monotone_semilength

added theorem DyckWord.nest_insidePart_add_outsidePart

added theorem DyckWord.nest_ne_zero

added def DyckWord.outsidePart

added theorem DyckWord.outsidePart_nest_add

added theorem DyckWord.outsidePart_zero

added theorem DyckWord.semilength_insidePart_add_semilength_outsidePart_add_one

added theorem DyckWord.semilength_insidePart_lt

added theorem DyckWord.semilength_outsidePart_lt

added theorem DyckWord.strictMono_semilength

added theorem DyckWord.toList_ne_nil

added theorem DyckWord.zero_le

added def Mathlib.Meta.Positivity.evalDyckWordFirstReturn