OAI/NumberTheory/Ostmann/Arithmetic/MovingDenominators.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_denominator line 10
2. theorem OAI.Ostmann.movingNodeGuard_denominators line 21
3. theorem OAI.Ostmann.movingNode_residuePeriod line 34

   Source documentation

   The three residue tests cost only powers of the existing ancestor denominators, one compensation product, and the actual node frequencies.

   theorem movingNode_residuePeriod {σ : Type*}
       (step : MovingSlotReversal σ) (value : σ → ℕ) (hs : step.rootFrequency ≠ 0)
       (hu : MovingSlotReversal.naturalProduct value step.compensationSlots ≠ 0)
       (childBound pivotBound : ℕ) (L R : HistoryFormula Bool) :
       ({ guard := movingNodeGuard (MovingSlotReversal.naturalProduct value step.leftSlots)
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.HistoryFormula, OAI.Ostmann.movingNodeGuard