IndexedRuns.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Indexed run starts retain the constant intervals needed for quotient paths.

def OAI.TwoPointCorrelations.IndexedRunStep line 16
theorem OAI.TwoPointCorrelations.scanRunTransitions_chain line 22
Source documentation
The scan retains the complete constant interval between consecutive run starts, not just the unequal labels.
```
theorem scanRunTransitions_chain (label : ℕ → α) (a n len : ℕ) (i : α)
    (han : a < n) (hcurrent : label a = i)
    (hconst : ∀ t ∈ Ico a n, label t = i) :
    ((a, i) :: scanRunTransitions label n len i).IsChain (IndexedRunStep label) := by
…
```
Mentions: OAI.TwoPointCorrelations.scanRunTransitions, OAI.TwoPointCorrelations.IndexedRunStep

theorem OAI.TwoPointCorrelations.scanRunTransitions_mem line 47

Source documentation

Labels in a scan agree with the actual numerical positions they record.

theorem scanRunTransitions_mem (label : ℕ → α) (n len : ℕ) (previous : α)
    (p : ℕ × α) (hp : p ∈ scanRunTransitions label n len previous) :
    n ≤ p.1 ∧ p.1 < n + len ∧ label p.1 = p.2 := by
…

Mentions: OAI.TwoPointCorrelations.scanRunTransitions

def OAI.TwoPointCorrelations.indexedBlockRuns line 63
theorem OAI.TwoPointCorrelations.indexedBlockRuns_chain line 68
theorem OAI.TwoPointCorrelations.indexedBlockRuns_mem line 78
def OAI.TwoPointCorrelations.blockLabelList line 90
lemma OAI.TwoPointCorrelations.blockLabelList_succ line 94
lemma OAI.TwoPointCorrelations.scanRunTransitions_labels line 103
theorem OAI.TwoPointCorrelations.indexedBlockRuns_labels line 116
Source documentation
Forgetting positions recovers precisely the run list used by the decoder.
```
theorem indexedBlockRuns_labels (label : ℕ → α) (start len : ℕ) :
    (indexedBlockRuns label start len).map Prod.snd =
      columnRunHeads ((blockLabelList label start len).map some) none := by
…
```
Mentions: OAI.TwoPointCorrelations.indexedBlockRuns, OAI.TwoPointCorrelations.columnRunHeads, OAI.TwoPointCorrelations.blockLabelList
theorem OAI.TwoPointCorrelations.indexedBlockRuns_partition line 128
Source documentation
Thus cutting indexed runs into regular segments yields exactly the same label pieces as cutting the decoder's compressed block.
```
theorem indexedBlockRuns_partition (label : ℕ → α) (start len : ℕ) (omitted : α → Bool) :
    (partitionColumnRuns (fun p => omitted p.2) (indexedBlockRuns label start len)).map
        (Sum.map (List.map Prod.snd) Prod.snd) =
      partitionColumnRuns omitted (columnRunHeads ((blockLabelList label start len).map some) none) := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns, OAI.TwoPointCorrelations.indexedBlockRuns, OAI.TwoPointCorrelations.columnRunHeads, OAI.TwoPointCorrelations.blockLabelList