MovingTemplateProducts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact moduli of the regular-slot templates

theorem OAI.Ostmann.naturalProduct_bulkSlotLeaves line 11

theorem OAI.Ostmann.movingTemplate_product line 27

Source documentation

Every regular coordinate occurs once in the small/bulk leaf lists.

theorem movingTemplate_product {A : Type*} (value : A → ℕ) (n r m : ℕ)
    (y : MovingRegularSlot n r m → A) :
    MovingSlotReversal.naturalProduct (value ∘ y)
      (flattenMovingSlots n (movingTemplateSmall n r m) ++
        flattenMovingSlots n (bulkSlotLeaves n m (movingTemplateBulk n r m))) =
      ∏ i, value (y i) := by
…

Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingTemplateSmall, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.movingTemplateBulk

theorem OAI.Ostmann.movingRestoreSample_product line 43
Source documentation
The extracted compensation modulus is exactly the factor removed from one child's complete regular modulus.
```
theorem movingRestoreSample_product {A : Type*} (value : A → ℕ) (n r m : ℕ)
    (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A) :
    (∏ i, value (movingRestoreSample n r m u y i)) =
      (∏ i, value (u i)) * ∏ i, value (y i) := by
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample