ColumnChunks.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Cutting actual perfect blocks and preserving their exact run lists.

def OAI.TwoPointCorrelations.columnFinalState line 14

Source documentation

The previous label after reading a finite part of a column.

def columnFinalState : List (Option α × Bool) → Option α → Option α
  | [], previous => previous
  | (a, _) :: rest, _ => columnFinalState rest a

/-- Streaming run compression composes at any cut, including imperfect entries. -/

theorem OAI.TwoPointCorrelations.columnRunHeadsWithCuts_append line 19
Source documentation
Streaming run compression composes at any cut, including imperfect entries.
```
theorem columnRunHeadsWithCuts_append (l r : List (Option α × Bool)) (previous : Option α) :
    columnRunHeadsWithCuts (l ++ r) previous =
      columnRunHeadsWithCuts l previous ++
        columnRunHeadsWithCuts r (columnFinalState l previous) := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeadsWithCuts, OAI.TwoPointCorrelations.columnFinalState
def OAI.TwoPointCorrelations.perfectBlockCuts line 34
Source documentation
Mark every entry of a perfect block, forcing its first run to start afresh.
```
def perfectBlockCuts : List α → List (Option α × Bool)
  | [] => []
  | a :: rest => (some a, true) :: rest.map (fun b => (some b, false))
```
theorem OAI.TwoPointCorrelations.plainBlock_heads line 38
theorem OAI.TwoPointCorrelations.perfectBlockCuts_heads line 48
Source documentation
A perfect block has its usual compressed run list regardless of the label just before it. Thus equal labels across block boundaries stay distinct runs.
```
theorem perfectBlockCuts_heads (l : List α) (previous : Option α) :
    columnRunHeadsWithCuts (perfectBlockCuts l) previous =
      columnRunHeads (l.map some) none := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeadsWithCuts, OAI.TwoPointCorrelations.perfectBlockCuts, OAI.TwoPointCorrelations.columnRunHeads
def OAI.TwoPointCorrelations.columnChunkCuts line 56
Source documentation
An actual column is a sequence of perfect blocks and individual imperfect entries.
```
def columnChunkCuts (chunks : List (List α ⊕ α)) : List (Option α × Bool) :=
…
```
def OAI.TwoPointCorrelations.columnChunkEntries line 59
def OAI.TwoPointCorrelations.columnChunkRuns line 62
theorem OAI.TwoPointCorrelations.perfectBlockCuts_values line 66
theorem OAI.TwoPointCorrelations.columnChunkCuts_values line 71
theorem OAI.TwoPointCorrelations.columnChunkCuts_heads line 83
Source documentation
Compression of the assembled column is exactly the concatenation of its independently compressed perfect blocks.
```
theorem columnChunkCuts_heads (chunks : List (List α ⊕ α)) (previous : Option α) :
    columnRunHeadsWithCuts (columnChunkCuts chunks) previous = columnChunkRuns chunks := by
…
```
Mentions: OAI.TwoPointCorrelations.columnRunHeadsWithCuts, OAI.TwoPointCorrelations.columnChunkCuts, OAI.TwoPointCorrelations.columnChunkRuns
def OAI.TwoPointCorrelations.columnChunkPieces line 97
Source documentation
Apply the omitted-label cut to every actual compressed perfect block.
```
def columnChunkPieces (omitted : α → Bool) (chunks : List (List α ⊕ α)) :
    List (List α ⊕ α) :=
…
```
theorem OAI.TwoPointCorrelations.columnChunkPieces_flatten line 102