ColumnChunkBudgets.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact decoder budgets for lists of actual perfect blocks.

theorem OAI.TwoPointCorrelations.regularPieceCount_append line 15
theorem OAI.TwoPointCorrelations.omittedPieceCount_append line 20

theorem OAI.TwoPointCorrelations.block_omitted_piece_budget line 25

Source documentation

Interval-shaped label occurrences imply the concrete omitted-run budget.

theorem block_omitted_piece_budget (l : List α) (omitted : Finset α)
    (hinterval : ∀ i j k : Fin l.length, i ≤ j → j ≤ k →
      l.get i = l.get k → l.get j = l.get i) :
    omittedPieceCount (partitionColumnRuns (fun a => decide (a ∈ omitted))
      (columnRunHeads (l.map some) none)) ≤ omitted.card := by
…

Mentions: OAI.TwoPointCorrelations.omittedPieceCount, OAI.TwoPointCorrelations.partitionColumnRuns, OAI.TwoPointCorrelations.columnRunHeads

theorem OAI.TwoPointCorrelations.block_regular_piece_budget line 39
def OAI.TwoPointCorrelations.perfectChunkCount line 52

theorem OAI.TwoPointCorrelations.columnChunk_piece_budgets line 57

Source documentation

Across actual perfect blocks, each omitted class is charged only once per block, and every regular segment is charged to an omitted run or a block start.

theorem columnChunk_piece_budgets (chunks : List (List α ⊕ α)) (omitted : Finset α)
    (hinterval : ∀ l, Sum.inl l ∈ chunks → ∀ i j k : Fin l.length, i ≤ j → j ≤ k →
      l.get i = l.get k → l.get j = l.get i) :
    omittedPieceCount (columnChunkPieces (fun a => decide (a ∈ omitted)) chunks) ≤
        omitted.card * perfectChunkCount chunks ∧
    regularPieceCount (columnChunkPieces (fun a => decide (a ∈ omitted)) chunks) ≤
        (omitted.card + 1) * perfectChunkCount chunks := by
…

Mentions: OAI.TwoPointCorrelations.omittedPieceCount, OAI.TwoPointCorrelations.columnChunkPieces, OAI.TwoPointCorrelations.perfectChunkCount, OAI.TwoPointCorrelations.regularPieceCount

theorem OAI.TwoPointCorrelations.columnChunkPieces_length_le line 92
Source documentation
The full merge mask fits in the original column length.
```
theorem columnChunkPieces_length_le (omitted : α → Bool) (chunks : List (List α ⊕ α)) :
    (columnChunkPieces omitted chunks).length ≤ (columnChunkEntries chunks).length := by
…
```
Mentions: OAI.TwoPointCorrelations.columnChunkPieces, OAI.TwoPointCorrelations.columnChunkEntries