OAI/NumberTheory/Ostmann/Arithmetic/MovingFrequencyModulus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPairFrequencyBase line 12
2. def OAI.Ostmann.movingPairFrequencyModulus line 15
3. theorem OAI.Ostmann.movingPairFrequencyBase_dvd line 18
4. theorem OAI.Ostmann.movingPairFrequencyModulus_precision line 25
5. theorem OAI.Ostmann.movingPairFrequencyModulus_pos line 32
6. theorem OAI.Ostmann.movingPairFrequencyModulus_bound line 40
7. theorem OAI.Ostmann.movingPairFrequencyModulus_exp line 50
8. theorem OAI.Ostmann.movingPattern_frequency_modulus line 65

   Source documentation

   The hypotheses on the original frequency list supply all frequency period and nonzero-modulus requirements of the prime comparison.

   theorem movingPattern_frequency_modulus {B C : Type*} {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
       (small : Bool → TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
       (pattern : Bool × MovingSampleIndex n → C)
       (hf : ∀ b, ∀ s ∈ allFrequencyList n (t b), s ≠ 0) :
       let T := movingPatternFinBulkData e n m t small slot perm pattern
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.allFrequencyList, OAI.Ostmann.movingPatternFinBulkData