RunCoverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Every observed regular class is present in an encoded regular segment.

theorem OAI.TwoPointCorrelations.columnRunHeads_cover line 14
Source documentation
Greedy compression can suppress only the preceding label; no observed class disappears from the previous-label/run-head pair.
```
theorem columnRunHeads_cover (l : List α) (previous : Option α) (a : α) (ha : a ∈ l) :
    previous = some a ∨ a ∈ columnRunHeads (l.map some) previous := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeads
theorem OAI.TwoPointCorrelations.mem_columnRunHeads line 33
theorem OAI.TwoPointCorrelations.partitionColumnRuns_regular_cover line 40
Source documentation
A regular observed run occurs in one of the actual regular pieces, so the shared forest numbering applies to it.
```
theorem partitionColumnRuns_regular_cover (omitted : α → Bool) (runs : List α)
    (a : α) (ha : a ∈ runs) (hregular : omitted a = false) :
    ∃ segment, Sum.inl segment ∈ partitionColumnRuns omitted runs ∧ a ∈ segment := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns