OAI/NumberTheory/Ostmann/Construction/SelectedBulkCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Bulk coordinates inside a larger word

The selected bulk slots are copied with the whole word. The top slot is retained in that word but belongs to the complementary matching block.

  1. def OAI.Ostmann.selectedBulkH line 14
  2. abbrev OAI.Ostmann.SelectedNonbulkH line 26
  3. def OAI.Ostmann.selectedBulkCoordinates line 30
  4. def OAI.Ostmann.selectedSplitHCoordinates line 36
  5. def OAI.Ostmann.selectedBulkLabel line 42
  6. theorem OAI.Ostmann.selectedBulkLabel_coordinates line 47
  7. def OAI.Ostmann.selectedSeparatedMatching line 61
  8. theorem OAI.Ostmann.selectedSeparatedMatching_injective line 78
  9. theorem OAI.Ostmann.selectedSplitHCoordinates_inl line 89
  10. theorem OAI.Ostmann.selectedBulkMatching_slot line 94
  11. theorem OAI.Ostmann.mem_selectedBulkH_of_origin line 107

    Source documentation

    An H slot over an original bulk position is one of the selected leaves.

    theorem mem_selectedBulkH_of_origin {I : Type*} (role : I → CopyScheduleRole)
    (n m : ℕ) (bulk : Fin m ↪ I) (hbulk : ∀ i, role (bulk i) = .word)
    (h : CopyScheduleH role n) (i : Fin m) (hi : copyScheduleOrigin n h.val = bulk i) :
    h ∈ Set.range (selectedBulkH role n m bulk hbulk) := by
…

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.selectedBulkH

  12. theorem OAI.Ostmann.selectedNonbulkH_card_active line 124