RegularFamilyNames.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Every regular perfect class inherits the bounds and injectivity of its forest line.

theorem OAI.TwoPointCorrelations.perfect_label_entry line 13
theorem OAI.TwoPointCorrelations.perfect_label_position line 24

theorem OAI.TwoPointCorrelations.regular_family_name_properties line 39

Source documentation

Coverage makes the shared forest bounds and injectivity apply to every perfect regular occurrence, including those suppressed by run compression.

theorem regular_family_name_properties (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ) (lineNumber : α → ℕ)
    (hnumber : ∀ z (hz : z ∈ regular), lineNumber z = number ⟨z, hz⟩)
    (labelNat : ℕ → α)
    (chunks : List (List α ⊕ α)) (blocks : List (ℕ × ℕ))
    (hentries : columnChunkEntries chunks =
      (columnPositionEntries perfect).map (fun p => (label p.1, p.2)))
    (hblocks : chunks.filterMap (Sum.elim some (fun _ => none)) =
      blocks.map (fun b => blockLabelList labelNat b.1 b.2))
    (hbound : ∀ segment ∈ indexedRegularSegments labelNat (fun z => decide (z ∉ regular)) blocks,
      ∀ p ∈ segment, lineNumber p.2 < N)
    (hinj : ∀ segment ∈ indexedRegularSegments labelNat (fun z => decide (z ∉ regular)) blocks,
…

Mentions: OAI.TwoPointCorrelations.columnChunkEntries, OAI.TwoPointCorrelations.columnPositionEntries, OAI.TwoPointCorrelations.blockLabelList, OAI.TwoPointCorrelations.indexedRegularSegments