Merging adjacent equal letters

This file isolates the run-merging operation used in the deduction of Proposition 5.7 from Proposition 5.9, paper equations (5.34)--(5.37). mergeEqualRuns keeps one representative of every maximal constant run. The generic listChainProduct_mergeEqualRuns lemma records the analytic reason this operation is harmless: an edge joining two equal letters has weight one.

def Anderson4D.mergeEqualRuns {α : Type u_1} [DecidableEq α] (l : List α) : List α

Keep exactly one representative of every maximal constant run.

Equations

• Anderson4D.mergeEqualRuns l = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) l

theorem Anderson4D.mergeEqualRuns_sublist {α : Type u_1} [DecidableEq α] (l : List α) : (mergeEqualRuns l).Sublist l

theorem Anderson4D.mergeEqualRuns_isChain {α : Type u_1} [DecidableEq α] (l : List α) : List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) (mergeEqualRuns l)

@[simp]

theorem Anderson4D.mergeEqualRuns_eq_nil {α : Type u_1} [DecidableEq α] {l : List α} : mergeEqualRuns l = [] ↔ l = []

theorem Anderson4D.mergeEqualRuns_length_le {α : Type u_1} [DecidableEq α] (l : List α) : (mergeEqualRuns l).length ≤ l.length

theorem Anderson4D.mergeEqualRuns_count_le {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : List.count a (mergeEqualRuns l) ≤ List.count a l

@[simp]

theorem Anderson4D.mem_mergeEqualRuns_iff {α : Type u_1} [DecidableEq α] (x : α) (l : List α) : x ∈ mergeEqualRuns l ↔ x ∈ l

def Anderson4D.listChainProduct {α : Type u_1} {R : Type u_2} [Monoid R] (edge : α → α → R) : List α → R

Consecutive-edge product on a list.

Equations

• Anderson4D.listChainProduct edge [] = 1
• Anderson4D.listChainProduct edge [head] = 1
• Anderson4D.listChainProduct edge (a :: b :: l) = edge a b * Anderson4D.listChainProduct edge (b :: l)

theorem Anderson4D.listChainProduct_eq_zipWith {α : Type u_1} {R : Type u_2} [Monoid R] (edge : α → α → R) (l : List α) : listChainProduct edge l = (List.zipWith edge l l.tail).prod

listChainProduct is the product of edge over the list zipped with its tail.

theorem Anderson4D.listChainProduct_map {α : Type u_1} {R : Type u_2} {β : Type u_3} [Monoid R] (edge : β → β → R) (f : α → β) (l : List α) : listChainProduct edge (List.map f l) = listChainProduct (fun (a b : α) => edge (f a) (f b)) l

Mapping the vertices of a chain is the same as precomposing its edge weight in both arguments.

theorem Anderson4D.listChainProduct_mergeEqualRuns {α : Type u_1} {R : Type u_2} [DecidableEq α] [Monoid R] (edge : α → α → R) (hdiag : ∀ (a : α), edge a a = 1) (l : List α) : listChainProduct edge (mergeEqualRuns l) = listChainProduct edge l

Merging equal runs preserves any chain product whose equal-letter edge weight is one.

def Anderson4D.mergedWordList {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) : List α

List form of a word after all adjacent equal letters have been merged.

Equations

• Anderson4D.mergedWordList w = Anderson4D.mergeEqualRuns (List.ofFn w)

def Anderson4D.mergedMultiplicity {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (a : α) : ℕ

Multiplicity of a letter after run merging.

Equations

• Anderson4D.mergedMultiplicity w a = List.count a (Anderson4D.mergedWordList w)

def Anderson4D.mergedWord {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) : Fin (mergedWordList w).length → α

The compressed word, indexed by its (generally smaller) length.

Equations

• Anderson4D.mergedWord w = (Anderson4D.mergedWordList w).get

theorem Anderson4D.mergedWordList_length_le {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) : (mergedWordList w).length ≤ m

theorem Anderson4D.mergedMultiplicity_le_originalCount {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (a : α) : mergedMultiplicity w a ≤ List.count a (List.ofFn w)

theorem Anderson4D.mergedMultiplicity_pos_iff {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (a : α) : 0 < mergedMultiplicity w a ↔ ∃ (i : Fin m), w i = a

theorem Anderson4D.mergedWord_mem_validWords {α : Type u_1} [DecidableEq α] {m : ℕ} [Fintype α] (w : Fin m → α) : mergedWord w ∈ validWords (mergedMultiplicity w)

The compressed word has the compressed multiplicities by construction.

theorem Anderson4D.sum_mergedMultiplicity {α : Type u_1} [DecidableEq α] {m : ℕ} [Fintype α] (w : Fin m → α) : ∑ a : α, mergedMultiplicity w a = (mergedWordList w).length

The new multiplicities sum to the compressed word length.

theorem Anderson4D.mergedWord_noAdjacentEqual {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) : NoAdjacentEqual (mergedWord w)

Adjacent letters of the compressed word are distinct.

theorem Anderson4D.mergedWordList_chainProduct {α : Type u_1} {R : Type u_2} [DecidableEq α] {m : ℕ} [Monoid R] (edge : α → α → R) (hdiag : ∀ (a : α), edge a a = 1) (w : Fin m → α) : listChainProduct edge (mergedWordList w) = listChainProduct edge (List.ofFn w)

Word-level form of run-merging invariance for a generic edge product.