OAI/NumberTheory/Ostmann/ZeroDensity/ProgressionWithoutPage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Progression estimates and the Page theorem

The fields specify exceptional zeros and the prime progression estimate from Montgomery–Vaughan, Theorem 11.3 and Corollary 11.20. Page uniqueness is Corollary 11.10.

  1. structure OAI.Ostmann.PublishedProgressionEstimate line 14
  2. def OAI.Ostmann.PublishedProgressionEstimate.toPublished line 31