OAI/NumberTheory/Ostmann/Construction/PreorderTransferPaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.transferNodeAtPath line 11
2. theorem OAI.Ostmann.transferNodeList_get_path line 21

   Source documentation

   Path lookup and the literal preorder list name the same node.

   theorem transferNodeList_get_path {State : Type*} (sys : TransferHistorySystem State)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) (path : List Bool)
       (hp : path.length < n) (fallback : ReconstructedTransferNode State) :
       (transferNodeList sys n σ t).getD (nodePathIndex n path) fallback =
         transferNodeAtPath sys n σ t path := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ReconstructedTransferNode, OAI.Ostmann.transferNodeList, OAI.Ostmann.nodePathIndex, OAI.Ostmann.transferNodeAtPath

3. theorem OAI.Ostmann.transferNodeAtPath_valid line 48
4. def OAI.Ostmann.replayNodeIndices line 57
5. theorem OAI.Ostmann.replayNodeIndices_actual line 65

   Source documentation

   The node's state is obtained by substituting just its proper ancestor pivots, in their root-to-leaf order.

   theorem replayNodeIndices_actual {State : Type*} (sys : TransferHistorySystem State)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) (path : List Bool)
       (hp : path.length < n) (d : ℕ) (p : ℕ → ℕ)
       (hanc : ∀ k < path.length, p (d + k) =
         (transferNodeAtPath sys n σ t (path.take k)).pivot sys) :
       replayNodeIndices sys path d p σ = (transferNodeAtPath sys n σ t path).state := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.transferNodeAtPath, OAI.Ostmann.replayNodeIndices