OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateLeaves.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.treeLeafTupleEquiv_append_slots line 11
2. theorem OAI.Ostmann.treeLeafTupleEquiv_compensation_slots line 21
3. theorem OAI.Ostmann.movingRestoreSample_small_leaves line 33

   Source documentation

   Restoring the same compensation sample in every surviving leaf gives exactly the small list required by the two child recursions.

   theorem movingRestoreSample_small_leaves {A : Type*} (n r m : ℕ)
       (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A) :
       treeLeafMap (List.map (movingRestoreSample n r m u y)) n (movingTemplateSmall n (4 + r) m) =
         appendMovingSlotLeaves n
           (movingCompensationSlots n ((treeLeafTupleEquiv (Fin 4 → A) n).symm
             (fun j i => u (j, i))))
           (treeLeafMap (List.map y) n (movingTemplateSmall n r m)) := by
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingRestoreSample, OAI.Ostmann.movingTemplateSmall, OAI.Ostmann.appendMovingSlotLeaves, OAI.Ostmann.movingCompensationSlots, OAI.Ostmann.treeLeafTupleEquiv

4. theorem OAI.Ostmann.movingRestoreSample_bulk_leaves line 54