Counting expansions of a run-compressed word

This module supplies the finite-fiber count needed in the deduction of Proposition 5.7 from Proposition 5.9. Once the compressed word is fixed, an original word is determined by the positive lengths of its constant runs. Those lengths form an ordinary composition of the original word length, so every compression fiber has cardinality at most 2 ^ M.

Run-length reconstruction

def Anderson4D.expandRunLengths {α : Type u_1} (representatives : List α) (lengths : List ℕ) : List α

Expand a list of run representatives using the corresponding list of run lengths. Mismatched tails are ignored by zipWith; all applications below carry an equality of the two list lengths.

Equations

• Anderson4D.expandRunLengths representatives lengths = (List.zipWith (fun (a : α) (n : ℕ) => List.replicate n a) representatives lengths).flatten

@[simp]

theorem Anderson4D.expandRunLengths_nil_left {α : Type u_1} (lengths : List ℕ) : expandRunLengths [] lengths = []

@[simp]

theorem Anderson4D.expandRunLengths_nil_right {α : Type u_1} (representatives : List α) : expandRunLengths representatives [] = []

@[simp]

theorem Anderson4D.expandRunLengths_cons {α : Type u_1} (a : α) (n : ℕ) (representatives : List α) (lengths : List ℕ) : expandRunLengths (a :: representatives) (n :: lengths) = List.replicate n a ++ expandRunLengths representatives lengths

theorem Anderson4D.mergeEqualRuns_cons_eq_cons {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : ∃ (tail : List α), mergeEqualRuns (a :: l) = a :: tail

A compressed nonempty list still starts with the original first letter.

theorem Anderson4D.exists_composition_expandRunLengths_mergeEqualRuns {α : Type u_1} [DecidableEq α] (l : List α) : ∃ (c : Composition l.length), c.blocks.length = (mergeEqualRuns l).length ∧ expandRunLengths (mergeEqualRuns l) c.blocks = l

Every list is obtained from its run-compressed list by a positive composition of its length.

Composition coordinates on finite words

theorem Anderson4D.exists_mergedRunComposition {α : Type u_1} [DecidableEq α] {M : ℕ} (w : Fin M → α) : ∃ (c : Composition M), c.blocks.length = (mergedWordList w).length ∧ expandRunLengths (mergedWordList w) c.blocks = List.ofFn w

Finite-word form of the run-length reconstruction theorem.

noncomputable def Anderson4D.mergedRunComposition {α : Type u_1} [DecidableEq α] {M : ℕ} (w : Fin M → α) : Composition M

A chosen positive run-length vector for a finite word. Its two specification lemmas below, rather than the choice itself, are the public interface.

Equations

• Anderson4D.mergedRunComposition w = Classical.choose ⋯

@[simp]

theorem Anderson4D.mergedRunComposition_blocks_length {α : Type u_1} [DecidableEq α] {M : ℕ} (w : Fin M → α) : (mergedRunComposition w).blocks.length = (mergedWordList w).length

@[simp]

theorem Anderson4D.expandRunLengths_mergedRunComposition {α : Type u_1} [DecidableEq α] {M : ℕ} (w : Fin M → α) : expandRunLengths (mergedWordList w) (mergedRunComposition w).blocks = List.ofFn w

theorem Anderson4D.mergedRunComposition_injective_on_mergedWordList {α : Type u_1} [DecidableEq α] {M : ℕ} {s : Finset (Fin M → α)} {v : List α} : Function.Injective fun (w : ↥({w ∈ s | mergedWordList w = v})) => mergedRunComposition ↑w

Among words with one fixed compressed representative list, the chosen run-length composition is injective.

theorem Anderson4D.card_filter_mergedWordList_le_two_pow {α : Type u_1} [DecidableEq α] {M : ℕ} (s : Finset (Fin M → α)) (v : List α) : {w ∈ s | mergedWordList w = v}.card ≤ 2 ^ M

Every fixed-compressed-list fiber in any finite family of length-M words has cardinality at most 2 ^ M.

The prescribed multiplicity/compressed-word fiber

def Anderson4D.mergeExpansionFiber {α : Type u_1} [DecidableEq α] [Fintype α] {M K : ℕ} (ml sl : α → ℕ) (v : Fin K → α) : Finset (Fin M → α)

Original valid words with prescribed compressed multiplicity and prescribed compressed word list. Using List.ofFn v avoids any dependent cast between the varying compressed lengths.

Equations

• Anderson4D.mergeExpansionFiber ml sl v = {w ∈ Anderson4D.validWords ml | Anderson4D.mergedMultiplicity w = sl ∧ Anderson4D.mergedWordList w = List.ofFn v}

@[simp]

theorem Anderson4D.mem_mergeExpansionFiber_iff {α : Type u_1} [DecidableEq α] [Fintype α] {M K : ℕ} (ml sl : α → ℕ) (v : Fin K → α) (w : Fin M → α) : w ∈ mergeExpansionFiber ml sl v ↔ w ∈ validWords ml ∧ mergedMultiplicity w = sl ∧ mergedWordList w = List.ofFn v

theorem Anderson4D.card_mergeExpansionFiber_le_two_pow {α : Type u_1} [DecidableEq α] [Fintype α] {M K : ℕ} (ml sl : α → ℕ) (v : Fin K → α) : (mergeExpansionFiber ml sl v).card ≤ 2 ^ M

The exact fiber requested in the run-compression regrouping costs at most 2 ^ M. The bound is stronger than needed: validity, the value of sl, and the no-adjacent condition on v play no role in the count.

Generic nonnegative weighted regrouping

def Anderson4D.mergeOutcome {α : Type u_1} [DecidableEq α] {M : ℕ} (w : Fin M → α) : (α → ℕ) × List α

The nondependent key carried by a run-compressed word.

Equations

• Anderson4D.mergeOutcome w = (Anderson4D.mergedMultiplicity w, Anderson4D.mergedWordList w)

def Anderson4D.mergeOutcomeImage {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (s : Finset (Fin M → α)) : Finset ((α → ℕ) × List α)

The finite set of compression outcomes realized by a finite word family.

Equations

• Anderson4D.mergeOutcomeImage s = Finset.image Anderson4D.mergeOutcome s

theorem Anderson4D.card_filter_mergeOutcome_le_two_pow {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (s : Finset (Fin M → α)) (outcome : (α → ℕ) × List α) : {w ∈ s | mergeOutcome w = outcome}.card ≤ 2 ^ M

A fiber of the full compression outcome is no larger than the fiber obtained by retaining only its compressed representative list.

theorem Anderson4D.sum_comp_mergeOutcome_eq_sum_fibers {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (s : Finset (Fin M → α)) (F : (α → ℕ) × List α → ℝ) : ∑ w ∈ s, F (mergeOutcome w) = ∑ outcome ∈ mergeOutcomeImage s, ↑{w ∈ s | mergeOutcome w = outcome}.card * F outcome

Exact finite regrouping of a statistic that depends only on the compression outcome.

theorem Anderson4D.sum_comp_mergeOutcome_le_two_pow_mul_sum {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (s : Finset (Fin M → α)) (F : (α → ℕ) × List α → ℝ) (hF : ∀ outcome ∈ mergeOutcomeImage s, 0 ≤ F outcome) : ∑ w ∈ s, F (mergeOutcome w) ≤ 2 ^ M * ∑ outcome ∈ mergeOutcomeImage s, F outcome

Generic weighted run-compression bound. A nonnegative statistic on compressed outcomes loses at most 2 ^ M when pulled back and summed over any finite family of original words.

Primitivity transport

theorem Anderson4D.expandRunLengths_append {α : Type u_1} (representatives₁ representatives₂ : List α) (lengths₁ lengths₂ : List ℕ) (haligned : representatives₁.length = lengths₁.length) : expandRunLengths (representatives₁ ++ representatives₂) (lengths₁ ++ lengths₂) = expandRunLengths representatives₁ lengths₁ ++ expandRunLengths representatives₂ lengths₂

Run expansion distributes over an aligned concatenation.

theorem Anderson4D.forall_mem_expandRunLengths {α : Type u_1} (representatives : List α) (lengths : List ℕ) (P : α → Prop) (hP : ∀ a ∈ representatives, P a) (x : α) : x ∈ expandRunLengths representatives lengths → P x

A letter predicate holding on all run representatives holds throughout their expansion.

theorem Anderson4D.expandRunLengths_ne_nil {α : Type u_1} (representatives : List α) (lengths : List ℕ) (hrepr : representatives ≠ []) (haligned : representatives.length = lengths.length) (hpos : ∀ n ∈ lengths, 0 < n) : expandRunLengths representatives lengths ≠ []

Positive aligned run lengths make the expansion of a nonempty representative list nonempty.

theorem Anderson4D.exists_expandRunLengths_three_parts {α : Type u_1} (representatives pre mid post : List α) (lengths : List ℕ) (hrepr : representatives = pre ++ mid ++ post) (haligned : representatives.length = lengths.length) : ∃ (lengthsPre : List ℕ) (lengthsMid : List ℕ) (lengthsPost : List ℕ), lengths = lengthsPre ++ lengthsMid ++ lengthsPost ∧ pre.length = lengthsPre.length ∧ mid.length = lengthsMid.length ∧ post.length = lengthsPost.length ∧ expandRunLengths representatives lengths = expandRunLengths pre lengthsPre ++ expandRunLengths mid lengthsMid ++ expandRunLengths post lengthsPost

Split a length list along an aligned three-part decomposition of its representative list.

theorem Anderson4D.letterPositions_eq_Icc_of_ofFn_decompose {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (S : Finset α) (w : Fin M → α) (pre mid post : List α) (hdecompose : List.ofFn w = pre ++ mid ++ post) (hpre : ∀ x ∈ pre, x ∉ S) (hmid : ∀ x ∈ mid, x ∈ S) (hpost : ∀ x ∈ post, x ∉ S) (hmidNonempty : mid ≠ []) : ∃ (a : Fin M) (b : Fin M), a ≤ b ∧ letterPositions w S = Finset.Icc a b

Finite-word specialization of letterPositions_eq_Icc_of_decompose, avoiding dependent casts through (List.ofFn w).length.

theorem Anderson4D.mergedWord_noProperLeafBlock {α : Type u_1} [DecidableEq α] [Fintype α] {M : ℕ} (w : Fin M → α) (hprimitive : NoProperLeafBlock w) : NoProperLeafBlock (mergedWord w)

Inserting positive repetitions inside constant runs preserves the paper's no-proper-leaf-block condition. Thus run compression transports primitivity to the compressed word.