OAI/NumberTheory/Ostmann/Construction/InitialMovingSlots.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.InitialRetainedSlot line 10
2. def OAI.Ostmann.initialRetainedIndexEquiv line 13

   Source documentation

   The left giant is true; fixed cells precede bulk in the moving template.

   def initialRetainedIndexEquiv (b r : ℕ) :
       InitialRetainedSlot b r ⊕ InitialRetainedSlot b r ≃
         Bool ⊕ MovingRegularSlot 0 (r + r) (b + b) where
   …

   Mentions: OAI.Ostmann.InitialRetainedSlot, OAI.Ostmann.MovingRegularSlot

3. def OAI.Ostmann.initialCompleteIndexEquiv line 44

   Source documentation

   Separate all fixed spectators, then the two giants and the moving slots.

   def initialCompleteIndexEquiv (b d r : ℕ) :
       Fin (d + d) ⊕ (Bool ⊕ MovingRegularSlot 0 (r + r) (b + b)) ≃
         Fin ((b + (d + r) + 1) + (b + (d + r) + 1)) :=
   …

   Mentions: OAI.Ostmann.MovingRegularSlot

4. def OAI.Ostmann.initialMovingTuple line 53
5. theorem OAI.Ostmann.initialCompleteIndexEquiv_assemble line 59
6. theorem OAI.Ostmann.initial_reassembled_moving_tuple line 84
7. theorem OAI.Ostmann.initialMovingTuple_reindex line 106
8. theorem OAI.Ostmann.initialMovingTuple_product line 113