BlockFamilyDecoding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Identify the shared indexed path family with the actual decoder pieces.

theorem OAI.TwoPointCorrelations.columnChunkPieces_via_blocks line 12
theorem OAI.TwoPointCorrelations.columnChunkPieces_from_intervals line 28
theorem OAI.TwoPointCorrelations.indexedRegularSegments_labels line 38
Source documentation
Forgetting the stored run-start indices gives exactly the regular piece list consumed by the column decoder, in the same order.
```
theorem indexedRegularSegments_labels (label : ℕ → α) (omitted : α → Bool)
    (blocks : List (ℕ × ℕ)) :
    (indexedRegularSegments label omitted blocks).map (List.map Prod.snd) =
      (blocks.flatMap (fun b => partitionColumnRuns omitted
        (columnRunHeads ((blockLabelList label b.1 b.2).map some) none))).filterMap
          (Sum.elim some (fun _ => none)) := by
…
```
Mentions: OAI.TwoPointCorrelations.indexedRegularSegments, OAI.TwoPointCorrelations.partitionColumnRuns, OAI.TwoPointCorrelations.columnRunHeads, OAI.TwoPointCorrelations.blockLabelList
theorem OAI.TwoPointCorrelations.indexedRegularSegments_eq_regular_pieces line 54
theorem OAI.TwoPointCorrelations.perfect_entry_mem_block line 66
Source documentation
Every original perfect occurrence belongs to one of the actual perfect blocks. This includes occurrences immediately next to imperfect positions.
```
theorem perfect_entry_mem_block (chunks : List (List α ⊕ α)) (a : α)
    (ha : (a, true) ∈ columnChunkEntries chunks) :
    ∃ block, Sum.inl block ∈ chunks ∧ a ∈ block := by
…
```
Mentions: OAI.TwoPointCorrelations.columnChunkEntries

theorem OAI.TwoPointCorrelations.perfect_regular_entry_covered line 81

Source documentation

Every regular perfect label appears in the actual indexed path family.

theorem perfect_regular_entry_covered (label : ℕ → α) (omitted : α → Bool)
    (chunks : List (List α ⊕ α)) (blocks : List (ℕ × ℕ))
    (hblocks : chunks.filterMap (Sum.elim some (fun _ => none)) =
      blocks.map (fun b => blockLabelList label b.1 b.2))
    (a : α) (ha : (a, true) ∈ columnChunkEntries chunks) (hr : omitted a = false) :
    ∃ segment ∈ indexedRegularSegments label omitted blocks, ∃ p ∈ segment, p.2 = a := by
…

Mentions: OAI.TwoPointCorrelations.blockLabelList, OAI.TwoPointCorrelations.columnChunkEntries, OAI.TwoPointCorrelations.indexedRegularSegments