OAI/NumberTheory/Ostmann/Construction/WordTransferFullPeriod.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.allFrequencyList line 11
2. theorem OAI.Ostmann.frequencyRoot_mem_allFrequencyList line 15
3. theorem OAI.Ostmann.internalFrequencyList_subset_all line 19
4. theorem OAI.Ostmann.allFrequencyList_length line 31
5. theorem OAI.Ostmann.WordTransferTemplate.guards_frequencies_mem line 40
6. def OAI.Ostmann.wordTransferFullPeriod line 60
7. theorem OAI.Ostmann.wordTransferFullPeriod_pos line 64
8. theorem OAI.Ostmann.WordTransferTemplate.guards_full_period line 72

   Source documentation

   Both units at every original node are periodic in this explicitly constructed modulus, including units modulo leaf frequencies.

   theorem WordTransferTemplate.guards_full_period {σ : Type*} {n : ℕ}
       (template : WordTransferTemplate σ n) (t : FrequencyTree ℤ n)
       (hn : NonzeroInternalFrequencies n t) (B : ℕ) (hB : 1 ≤ B)
       (hwords : template.WordsBounded B) :
       ∀ g ∈ template.guards t hn .prime,
         g.pivot.cleared.denominator * g.right.natAbs ∣ (wordTransferFullPeriod n t B : ℤ) ∧
         g.rightProduct.cleared.denominator * g.root.natAbs ∣ (wordTransferFullPeriod n t B : ℤ) := by
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.wordTransferFullPeriod

9. theorem OAI.Ostmann.wordTransferFullPeriod_le line 90
10. theorem OAI.Ostmann.prime_coprime_wordTransferFullPeriod line 102