CompressedRuns.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual constant-run compression of a perfect block.

theorem OAI.TwoPointCorrelations.destutter'_eq_columnRunHeads line 16
Source documentation
The decoder's greedy run heads are exactly the library's constant-run compression, so its sublist and adjacent-inequality properties apply.
```
theorem destutter'_eq_columnRunHeads (a : α) (l : List α) :
    l.destutter' (· ≠ ·) a = a :: columnRunHeads (l.map some) (some a) := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeads
theorem OAI.TwoPointCorrelations.columnRunHeads_eq_destutter line 26

theorem OAI.TwoPointCorrelations.sublist_chain_nodup_of_intervals line 37

Source documentation

A subsequence with unequal adjacent entries has no repeated label when all occurrences in the original block are interval-shaped.

theorem sublist_chain_nodup_of_intervals (l runs : List α) (hsub : runs.Sublist l)
    (hchain : runs.IsChain (· ≠ ·))
    (hinterval : ∀ i j k : Fin l.length, i ≤ j → j ≤ k →
      l.get i = l.get k → l.get j = l.get i) : runs.Nodup := by
…

theorem OAI.TwoPointCorrelations.columnRunHeads_nodup line 57
Source documentation
Each numerical label contributes at most one compressed run in a perfect block. This is proved for the actual run-head algorithm.
```
theorem columnRunHeads_nodup (l : List α)
    (hinterval : ∀ i j k : Fin l.length, i ≤ j → j ≤ k →
      l.get i = l.get k → l.get j = l.get i) :
    (columnRunHeads (l.map some) none).Nodup := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeads