RunSegments.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Interval-shaped label uses bound omitted runs and regular segments.

theorem OAI.TwoPointCorrelations.run_labels_injective line 16

Source documentation

A sequence obtained by keeping run starts has no repeated label when every label's original occurrences form an interval.

theorem run_labels_injective {m n : ℕ} (label : Fin n → α)
    (hinterval : ∀ i j k : Fin n, i ≤ j → j ≤ k → label i = label k → label j = label i)
    (start : Fin m → Fin n) (hstart : StrictMono start)
    (hchange : ∀ i j : Fin m, i.val + 1 = j.val → label (start i) ≠ label (start j)) :
    Function.Injective (label ∘ start) := by
…

theorem OAI.TwoPointCorrelations.fin_label_intervals line 36
def OAI.TwoPointCorrelations.omittedRunPositions line 44
theorem OAI.TwoPointCorrelations.omitted_runs_le line 48
Source documentation
One omitted label contributes at most one run in a perfect block.
```
theorem omitted_runs_le {m : ℕ} (label : Fin m → α) (omitted : Finset α)
    (hinj : Function.Injective label) :
    (omittedRunPositions label omitted).card ≤ omitted.card := by
…
```
Mentions: OAI.TwoPointCorrelations.omittedRunPositions
def OAI.TwoPointCorrelations.RegularRunStart line 59
Source documentation
A regular segment starts at the first run or immediately after an omitted run. Empty segments are not counted.
```
def RegularRunStart {m : ℕ} (label : Fin m → α) (omitted : Finset α) (i : Fin m) : Prop :=
…
```
def OAI.TwoPointCorrelations.regularRunStarts line 62
theorem OAI.TwoPointCorrelations.regular_segments_le line 69
Source documentation
Charge every noninitial regular segment to its immediately preceding omitted run. This argument allows any numerical values of the labels.
```
theorem regular_segments_le {m : ℕ} (label : Fin m → α) (omitted : Finset α) :
    (regularRunStarts label omitted).card ≤ (omittedRunPositions label omitted).card + 1 := by
…
```
Mentions: OAI.TwoPointCorrelations.regularRunStarts, OAI.TwoPointCorrelations.omittedRunPositions
theorem OAI.TwoPointCorrelations.regular_segments_le_omitted_labels line 98

theorem OAI.TwoPointCorrelations.block_run_budgets line 105

Source documentation

Across B perfect blocks these are the exact combinatorial budgets used in the endpoint and omitted-label parts of the forest code.

theorem block_run_budgets {B : ℕ} (m : Fin B → ℕ)
    (label : ∀ b, Fin (m b) → α) (omitted : Finset α)
    (hinj : ∀ b, Function.Injective (label b)) :
    (∑ b, (omittedRunPositions (label b) omitted).card) ≤ omitted.card * B ∧
    (∑ b, (regularRunStarts (label b) omitted).card) ≤ (omitted.card + 1) * B := by
…

Mentions: OAI.TwoPointCorrelations.omittedRunPositions, OAI.TwoPointCorrelations.regularRunStarts