OAI/NumberTheory/Ostmann/Construction/ScheduledNodeFrequencies.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ReconstructedTransferNode.frequencies line 10
2. theorem OAI.Ostmann.transferNodeList_frequencies line 14
3. theorem OAI.Ostmann.transferNodeArray_frequencies line 24
4. theorem OAI.Ostmann.scheduledNodeValues_valid line 36

   Source documentation

   Validity at a node now uses the frequency triple of that exact preorder entry, with no independently supplied node relation.

   theorem scheduledNodeValues_valid {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (S : Finset ℤ) (n : ℕ) (C : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree S n)
       (hv : ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) n ⟨n, C⟩
         (frequencyTreeMap Subtype.val n t)) (j : Fin (2 ^ n - 1)) :
       let p := transferPivotArray (scheduleAtomSystem role childBound pivotBound) n ⟨n, C⟩
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.transferPivotArray