OAI/NumberTheory/Ostmann/Preliminaries/MertensPrimeBands.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact published Mertens input for logarithmic prime bands

F. Mertens, J. reine angew. Math. 78 (1874), 46–62, first theorem, DOI 10.1515/crll.1874.78.46. Both sides of the bounded-error estimate are needed to subtract the lower cutoff; the collision argument uses only its previously recorded lower-bound consequence.

  1. def OAI.Ostmann.MertensEstimate line 18
  2. theorem OAI.Ostmann.MertensEstimate.lower line 21
  3. theorem OAI.Ostmann.MertensEstimate.upper line 26
  4. def OAI.Ostmann.logPrimeBand line 31
  5. theorem OAI.Ostmann.floor_exp_log_bounds line 34
  6. theorem OAI.Ostmann.logPrimeBand_mem line 50
  7. theorem OAI.Ostmann.logPrimeBand_weight_bounds line 65