OAI/NumberTheory/Ostmann/ZeroDensity/UniformPrimeProgressions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime intervals with one retained Page character

The second error below accounts for local exceptional zeros outside Page's common region. This derives simultaneous compatibility across moduli from the published zero uniqueness, rather than assuming compatibility of the short-interval estimates.

  1. theorem OAI.Ostmann.PublishedProgressionInput.uniform_log_interval line 18