OAI/NumberTheory/Ostmann/Construction/OriginalProductScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Product and frequency ranges for the concrete moment parameters

  1. theorem OAI.Ostmann.primeSubsetProducts_log_bounds line 11
  2. theorem OAI.Ostmann.original_prime_product_scale line 35
  3. theorem OAI.Ostmann.originalFrequencyCutoff_bounds line 61
  4. theorem OAI.Ostmann.originalFrequencyCutoff_covers line 76