RunPartition.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cutting a compressed perfect block into regular segments and omitted runs.

def OAI.TwoPointCorrelations.partitionColumnRuns line 13

Source documentation

Omitted labels stand alone; consecutive regular labels form one segment.

def partitionColumnRuns (omitted : α → Bool) : List α → List (List α ⊕ α)
  | [] => []
  | a :: rest =>
      if omitted a then .inr a :: partitionColumnRuns omitted rest
      else match partitionColumnRuns omitted rest with
        | .inl segment :: tail => .inl (a :: segment) :: tail
        | tail => .inl [a] :: tail

/-- Cutting does not reorder, omit or duplicate any compressed run. -/

theorem OAI.TwoPointCorrelations.partitionColumnRuns_flatten line 22
Source documentation
Cutting does not reorder, omit or duplicate any compressed run.
```
theorem partitionColumnRuns_flatten (omitted : α → Bool) (runs : List α) :
    (partitionColumnRuns omitted runs).flatMap (Sum.elim id List.singleton) = runs := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns
theorem OAI.TwoPointCorrelations.partitionColumnRuns_omitted line 36
Source documentation
The omitted part is exactly the original subsequence of omitted runs.
```
theorem partitionColumnRuns_omitted (omitted : α → Bool) (runs : List α) :
    (partitionColumnRuns omitted runs).filterMap (Sum.elim (fun _ => none) some) =
      runs.filter omitted := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns
theorem OAI.TwoPointCorrelations.partitionColumnRuns_length_le line 52
Source documentation
A merge mask needs no more slots than the compressed run list.
```
theorem partitionColumnRuns_length_le (omitted : α → Bool) (runs : List α) :
    (partitionColumnRuns omitted runs).length ≤ runs.length := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns
def OAI.TwoPointCorrelations.regularPieceCount line 69
def OAI.TwoPointCorrelations.omittedPieceCount line 72
def OAI.TwoPointCorrelations.startsWithRegularPiece line 75
theorem OAI.TwoPointCorrelations.partitionColumnRuns_count_strong line 80
Source documentation
Every regular segment except a possible initial one is charged to an omitted run. The stronger head-sensitive form makes the induction exact.
```
theorem partitionColumnRuns_count_strong (omitted : α → Bool) (runs : List α) :
    regularPieceCount (partitionColumnRuns omitted runs) ≤
      omittedPieceCount (partitionColumnRuns omitted runs) +
        if startsWithRegularPiece (partitionColumnRuns omitted runs) then 1 else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.regularPieceCount, OAI.TwoPointCorrelations.partitionColumnRuns, OAI.TwoPointCorrelations.omittedPieceCount, OAI.TwoPointCorrelations.startsWithRegularPiece
theorem OAI.TwoPointCorrelations.partitionColumnRuns_regular_count line 97