The global slot list

The participating flags of an edge subset, enumerated in slot order, and the link between the pattern inversion count and list inversions.

noncomputable def RS.partSlots (W : ClosedFragment) (F : EdgeSubset W) : Finset (Fin (edgeCount W + edgeCount W))

The set of slots whose flags participate in F.

Equations

• RS.partSlots W F = {q : Fin (RS.edgeCount W + RS.edgeCount W) | (RS.starFlagEnum W).symm q ∈ F.flags}

theorem RS.mem_partSlots {W : ClosedFragment} {F : EdgeSubset W} (q : Fin (edgeCount W + edgeCount W)) : q ∈ partSlots W F ↔ (starFlagEnum W).symm q ∈ F.flags

Membership in partSlots.

noncomputable def RS.globalSlotList (W : ClosedFragment) (F : EdgeSubset W) : List ↥F.flags

The global slot list: participating flags in slot order.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.globalSlotList_nodup (W : ClosedFragment) (F : EdgeSubset W) : (globalSlotList W F).Nodup

The global slot list is duplicate-free.

theorem RS.mem_globalSlotList (W : ClosedFragment) (F : EdgeSubset W) (x : ↥F.flags) : x ∈ globalSlotList W F

Every participating flag appears in the global slot list.

theorem RS.filter_length_ofFn {β : Type} {n : ℕ} (g : Fin n → β) (p : β → Bool) : (List.filter p (List.ofFn g)).length = {i : Fin n | p (g i) = true}.card

Filter length of ofFn matches finset card.

theorem RS.inversions_ofFn_eq_card {β : Type} [LinearOrder β] {n : ℕ} (g : Fin n → β) : inversions (List.ofFn g) = {p : Fin n × Fin n | p.1 < p.2 ∧ g p.2 < g p.1}.card

Inversion count of ofFn g equals the pair-filter card.

theorem RS.sortKey_symm_slot (W : ClosedFragment) (x : Fin (ds W).sum) : sortKey W ((starFlagEnum W).symm ((finCongr ⋯) ((sortSplitPerm W) x))) = x

The key of the flag at slot finCongr ... (sortSplitPerm W x) is x itself.

theorem RS.patternOddInv_eq_inversions (W : ClosedFragment) (F : EdgeSubset W) : patternOddInv W F = inversions (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (globalSlotList W F))

The pattern inversion count equals the key-inversions of the global slot list.