OAI/NumberTheory/Ostmann/Construction/ScheduledPreorderNodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.transferNodeArray line 12
2. def OAI.Ostmann.transferPivotArray line 17
3. theorem OAI.Ostmann.transferNodeArray_path line 21
4. theorem OAI.Ostmann.transferNodeArray_valid line 28
5. theorem OAI.Ostmann.replayNodeIndices_preorder line 34
6. def OAI.Ostmann.reversePathOfList line 45
7. theorem OAI.Ostmann.replayNodeIndices_schedule line 48
8. theorem OAI.Ostmann.scheduledNodeValues_actual line 75

   Source documentation

   The source-environment assignment is precisely the state of the actual preorder history node, with its actual reconstructed natural pivots.

   theorem scheduledNodeValues_actual {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (n : ℕ) (C : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n)
       (j : Fin (2 ^ n - 1)) :
       (transferNodeArray (scheduleAtomSystem role childBound pivotBound) n ⟨n, C⟩ t j).state =
         ⟨scheduledNodeLevel n j + 1, scheduledNodeValues role n j C
           (transferPivotArray (scheduleAtomSystem role childBound pivotBound) n ⟨n, C⟩ t)⟩ := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.transferNodeArray, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduledNodeLevel, OAI.Ostmann.scheduledNodeValues, OAI.Ostmann.transferPivotArray