OAI/NumberTheory/Ostmann/Construction/ExpandedScheduledTemplate.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.expandedHWord line 11
2. def OAI.Ostmann.expandedScheduledTemplate line 18

   Source documentation

   Actual atoms may have several prime constituents. An erased pivot is replaced by its single reconstructed total; all other atoms retain their lists.

   noncomputable def expandedScheduledTemplate {I σ : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (address : ℕ → List Bool → σ) (childBound pivotBound : ℕ → ℕ) :
       (n : ℕ) → List Bool → (CopyScheduleAtoms role n → List σ) → WordTransferTemplate σ n
     | 0, _, current => .leaf ((Finset.univ.toList : List (CopyScheduleAtoms role 0)).flatMap current)
     | n + 1, path, current =>
         .node ⟨address n path, expandedHWord role n true current, expandedHWord role n false current,
           childBound n, pivotBound n⟩
           (expandedScheduledTemplate role address childBound pivotBound n (true :: path)
             (reverseCopyLabelMap role n true [address n path] current))
           (expandedScheduledTemplate role address childBound pivotBound n (false :: path)
             (reverseCopyLabelMap role n false [address n path] current))

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.expandedHWord, OAI.Ostmann.reverseCopyLabelMap

3. theorem OAI.Ostmann.list_flatMap_length_bound line 30
4. theorem OAI.Ostmann.reverseCopyLabelMap_list_length line 40
5. theorem OAI.Ostmann.expandedHWord_length line 51
6. theorem OAI.Ostmann.expandedScheduledTemplate_words_bounded line 59
7. theorem OAI.Ostmann.list_flatMap_product line 85
8. theorem OAI.Ostmann.expandedHWord_product line 92