OAI/NumberTheory/Ostmann/Arithmetic/SingleFrequencyModulus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.historyFrequencyProduct line 13

   Source documentation

   The product includes every internal frequency and every leaf frequency, with multiplicity, exactly as in the residue-precision argument.

   def historyFrequencyProduct (S : Finset ℤ) : (n : ℕ) → FrequencyTree S n → ℕ
     | 0, s => (show S from s).val.natAbs
     | n + 1, t => (t.1 : ℤ).natAbs * historyFrequencyProduct S n t.2.1 *
         historyFrequencyProduct S n t.2.2

   Mentions: OAI.Ostmann.FrequencyTree

2. def OAI.Ostmann.historyFrequencyModulus line 18
3. theorem OAI.Ostmann.historyFrequencyProduct_pos line 21
4. theorem OAI.Ostmann.historyFrequencyModulus_pos line 29
5. theorem OAI.Ostmann.historyFrequencyProduct_le line 33
6. theorem OAI.Ostmann.historyFrequencyModulus_le line 48
7. theorem OAI.Ostmann.history_root_dvd_frequencyProduct line 54
8. theorem OAI.Ostmann.singleFrequencySplitList_root_mem line 64
9. theorem OAI.Ostmann.singleTreeNodeFrequencies_root_mem line 75
10. theorem OAI.Ostmann.history_node_dvd_frequencyProduct line 83
11. theorem OAI.Ostmann.history_node_dvd_frequencyModulus line 95
12. theorem OAI.Ostmann.prime_coprime_historyFrequencyModulus line 102

    Source documentation

    All actual primes exceed the frequency range. Consequently they are units for the full history modulus, including its precision exponent.

    theorem prime_coprime_historyFrequencyModulus (S : Finset ℤ) (N p : ℕ)
        (hp : p.Prime) (hpN : N < p)
        (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) (n k : ℕ) (t : FrequencyTree S n) :
        p.Coprime (historyFrequencyModulus S n k t) := by
    …

    Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyFrequencyModulus

13. theorem OAI.Ostmann.historyFrequencyModulus_le_exp line 119