OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternTemplateEnumeration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPatternTemplateSlots_eq line 11
2. def OAI.Ostmann.movingPatternTemplateEquiv line 17
3. theorem OAI.Ostmann.movingPatternTemplateEquiv_label line 24
4. theorem OAI.Ostmann.movingPatternTemplate_inactive_not_bulk line 36

   Source documentation

   The inactive-slot condition used by the arithmetic theorem follows from activity of the actual bulk slots.

   theorem movingPatternTemplate_inactive_not_bulk {C : Type*} {N : ℕ} (n r m : ℕ)
       (e : Fin (N + 1) ≃ MovingRegularSlot n r m ⊕ C)
       (active : MovingRegularSlot n r m → Bool)
       (hactive : ∀ j, active (movingTemplateBulk n r m j) = true)
       (i : Fin (movingPatternRegularSlots e n m (movingTemplateSmall n r m)
         (movingTemplateBulk n r m)).length)
       (hi : active (movingPatternTemplateEquiv n r m e i) = false) :
       (movingPatternRegularSlots e n m (movingTemplateSmall n r m)
         (movingTemplateBulk n r m)).get i ∉
         Set.range (movingPatternBulkEmbedding e (movingTemplateBulk n r m)) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateBulk, OAI.Ostmann.movingPatternRegularSlots, OAI.Ostmann.movingTemplateSmall, OAI.Ostmann.movingPatternTemplateEquiv, OAI.Ostmann.movingPatternBulkEmbedding