OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPermutedProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkSlotLeaves_perm_matching line 10
2. theorem OAI.Ostmann.movingPatternFinBulkData_regular_product_permuted line 30

   Source documentation

   A matching changes only the distribution of the bulk labels among leaves. The regular product of the complete tree is preserved, even when the sampled prime values have collisions.

   theorem movingPatternFinBulkData_regular_product_permuted {B C : Type*} {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
       (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
       (pattern : Bool × MovingSampleIndex n → C) (value : Fin (N + 1) → ℕ) (b : Bool) :
       MovingSlotReversal.naturalProduct value
         (movingPatternFinBulkData e n m t (fun _ => small) slot perm pattern b).regularSlots =
       MovingSlotReversal.naturalProduct value
         (flattenMovingSlots n (movingPatternFiniteSmall e n small) ++
           flattenMovingSlots n (bulkSlotLeaves n m (movingPatternBulkEmbedding e slot))) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.movingPatternFinBulkData, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingPatternFiniteSmall, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.movingPatternBulkEmbedding