RunPartitionProperties.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The omitted-label cut retains the actual adjacency of every regular segment.

theorem OAI.TwoPointCorrelations.partitionColumnRuns_regular_infix line 14
Source documentation
Every regular piece is a contiguous part of the original run list.
```
theorem partitionColumnRuns_regular_infix (omitted : α → Bool) (runs segment : List α)
    (hsegment : Sum.inl segment ∈ partitionColumnRuns omitted runs) :
    segment.IsInfix runs := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns

theorem OAI.TwoPointCorrelations.partitionColumnRuns_regular_chain line 24

Source documentation

Cutting out omitted runs does not create new adjacent pairs inside a piece.

theorem partitionColumnRuns_regular_chain (R : α → α → Prop)
    (omitted : α → Bool) (runs segment : List α) (hchain : runs.IsChain R)
    (hsegment : Sum.inl segment ∈ partitionColumnRuns omitted runs) :
    segment.IsChain R :=
…

Mentions: OAI.TwoPointCorrelations.partitionColumnRuns

theorem OAI.TwoPointCorrelations.partitionColumnRuns_regular_entries line 32
Source documentation
The cut algorithm produces only nonempty regular pieces, all of whose entries really are regular.
```
theorem partitionColumnRuns_regular_entries (omitted : α → Bool) (runs : List α) :
    ∀ segment, Sum.inl segment ∈ partitionColumnRuns omitted runs →
      segment ≠ [] ∧ ∀ a ∈ segment, omitted a = false := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns
theorem OAI.TwoPointCorrelations.partitionColumnRuns_map line 72
Source documentation
Run positions and their labels may be cut in parallel: the algorithm uses only the omitted predicate, so forgetting the positions commutes with it.
```
theorem partitionColumnRuns_map (f : α → β) (omitted : β → Bool) (runs : List α) :
    partitionColumnRuns omitted (runs.map f) =
      (partitionColumnRuns (fun a => omitted (f a)) runs).map (Sum.map (List.map f) f) := by
…
```
Mentions: OAI.TwoPointCorrelations.partitionColumnRuns