OAI/NumberTheory/Ostmann/Arithmetic/MovingRegularTemplate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.MovingRegularSlot line 12

   Source documentation

   Each surviving leaf has its remaining small slots and its original bulk.

   abbrev MovingRegularSlot (n r m : ℕ) := TreeLeafIndex n × (Fin r ⊕ Fin m)

   Mentions: OAI.Ostmann.TreeLeafIndex

2. def OAI.Ostmann.movingTemplateBulk line 14
3. def OAI.Ostmann.movingTemplateSmall line 18
4. theorem OAI.Ostmann.movingTemplateSmall_length line 21
5. theorem OAI.Ostmann.movingTemplateSmall_not_bulk line 24
6. theorem OAI.Ostmann.movingRegularSlot_card line 33
7. def OAI.Ostmann.movingReverseTemplate line 40

   Source documentation

   Restoring a removed type puts its four sampled compensation primes back before the surviving small slots. Bulk labels retain their identity.

   def movingReverseTemplate (n r m : ℕ) :
       ((TreeLeafIndex n × Fin 4) ⊕ MovingRegularSlot n r m) ≃ MovingRegularSlot n (4 + r) m where
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot

8. theorem OAI.Ostmann.movingReverseTemplate_bulk line 57
9. theorem OAI.Ostmann.movingReverseTemplate_compensation line 61