OAI/NumberTheory/Ostmann/Characters/RepeatedPrimePeriod.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sampledPrimeSet line 13
2. def OAI.Ostmann.primeSlotCount line 16
3. theorem OAI.Ostmann.primeSlotCount_pos line 19
4. theorem OAI.Ostmann.primeSlotCount_sum line 24
5. theorem OAI.Ostmann.formal_prime_product line 30
6. theorem OAI.Ostmann.all_multiple_prime_count line 36
7. theorem OAI.Ostmann.repeated_prime_period_bound line 44

   Source documentation

   A repeated label removes at least that prime from the formal period. This is the period saving used before bandlimited Poisson summation.

   theorem repeated_prime_period_bound {I : Type*} [Fintype I] (p : I → ℕ)
       (hp : ∀ i, 1 ≤ p i) {q : ℕ} (hq : q ∈ sampledPrimeSet p)
       (hm : 2 ≤ primeSlotCount p q) :
       q * (∏ r ∈ sampledPrimeSet p, r) ≤ ∏ i, p i := by
   …

   Mentions: OAI.Ostmann.sampledPrimeSet, OAI.Ostmann.primeSlotCount