PerfectBlockPartition.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Construct short perfect blocks from the actual position-status list.

def OAI.TwoPointCorrelations.initialColumnChunks line 12
theorem OAI.TwoPointCorrelations.initialColumnChunks_entries line 16
Source documentation
The initial cut preserves every label and its original perfect status.
```
theorem initialColumnChunks_entries (entries : List (α × Bool)) :
    columnChunkEntries (initialColumnChunks entries) = entries := by
…
```
Mentions: OAI.TwoPointCorrelations.columnChunkEntries, OAI.TwoPointCorrelations.initialColumnChunks
lemma OAI.TwoPointCorrelations.perfectChunkCount_map line 47
lemma OAI.TwoPointCorrelations.perfectChunkLength_le_entries line 54
theorem OAI.TwoPointCorrelations.initialColumnChunks_count line 65
Source documentation
Each maximal perfect interval is charged to a preceding imperfect position, except for a possible first interval.
```
theorem initialColumnChunks_count (entries : List (α × Bool)) :
    perfectChunkCount (initialColumnChunks entries) ≤
      (entries.filter (fun a => !a.2)).length + 1 := by
…
```
Mentions: OAI.TwoPointCorrelations.perfectChunkCount, OAI.TwoPointCorrelations.initialColumnChunks
def OAI.TwoPointCorrelations.shortPerfectColumnChunks line 72
theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_entries line 75
theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_count line 81
Source documentation
This is the explicit one-half version of the manuscript's perfect-block count. Applying it to both halves gives the stated absolute bound.
```
theorem shortPerfectColumnChunks_count (s : ℕ) (entries : List (α × Bool)) :
    perfectChunkCount (shortPerfectColumnChunks s entries) ≤
      entries.length / s + (entries.filter (fun a => !a.2)).length + 1 := by
…
```
Mentions: OAI.TwoPointCorrelations.perfectChunkCount, OAI.TwoPointCorrelations.shortPerfectColumnChunks