PerfectBlockPositions.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The constructed perfect blocks are actual contiguous intervals of positions.

theorem OAI.TwoPointCorrelations.subdivideColumnChunks_regular_origin line 12
theorem OAI.TwoPointCorrelations.initialColumnChunks_regular_origin line 23
theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_regular_positions line 36
Source documentation
Every constructed block is a contiguous part of the original column, and all its positions have their original perfect status.
```
theorem shortPerfectColumnChunks_regular_positions (s : ℕ) (entries : List (α × Bool))
    (block : List α) (hb : Sum.inl block ∈ shortPerfectColumnChunks s entries) :
    block.IsInfix (entries.map Prod.fst) ∧ ∀ a ∈ block, (a, true) ∈ entries := by
…
```
Mentions: OAI.TwoPointCorrelations.shortPerfectColumnChunks
theorem OAI.TwoPointCorrelations.blockLabelList_take line 54
Source documentation
A prefix of the position-indexed label list is the same label list with the shortened length.
```
theorem blockLabelList_take (label : ℕ → α) (start total len : ℕ) (h : len ≤ total) :
    (blockLabelList label start total).take len = blockLabelList label start len := by
…
```
Mentions: OAI.TwoPointCorrelations.blockLabelList
theorem OAI.TwoPointCorrelations.blockLabelList_drop_take line 65
theorem OAI.TwoPointCorrelations.infix_blockLabelList_positions line 80
Source documentation
Every contiguous part of a position-indexed list has an actual bounded starting index, so no extra run-position data need be postulated.
```
theorem infix_blockLabelList_positions (label : ℕ → α) (start total : ℕ)
    (block : List α) (hb : block.IsInfix (blockLabelList label start total)) :
    ∃ a, a + block.length ≤ total ∧ block = blockLabelList label (start + a) block.length := by
…
```
Mentions: OAI.TwoPointCorrelations.blockLabelList

theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_regular_size line 93

Source documentation

Each short block has the promised maximum length.

theorem shortPerfectColumnChunks_regular_size (s : ℕ) (hs : 0 < s)
    (entries : List (α × Bool)) (block : List α)
    (hb : Sum.inl block ∈ shortPerfectColumnChunks s entries) : block.length ≤ s := by
…

Mentions: OAI.TwoPointCorrelations.shortPerfectColumnChunks

theorem OAI.TwoPointCorrelations.shortPerfectColumnChunks_position_intervals line 102

Source documentation

On the actual consecutive position list, every generated block has a bounded starting index and contains only perfect positions.

theorem shortPerfectColumnChunks_position_intervals (N s : ℕ) (perfect : ℕ → Bool)
    (block : List ℕ)
    (hb : Sum.inl block ∈ shortPerfectColumnChunks s
      ((List.range N).map (fun i => (i, perfect i)))) :
    ∃ start, start + block.length ≤ N ∧
      block = (List.range block.length).map (fun i => start + i) ∧
      ∀ i ∈ block, perfect i = true := by
…

Mentions: OAI.TwoPointCorrelations.shortPerfectColumnChunks