OAI/NumberTheory/Ostmann/ZeroDensity/ProgressionPrincipalPNT.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The conductor-one consequence of the progression input

The principal smooth PNT is not an independent input: the conductor-one theta estimate, elementary prime-power removal and partial summation suffice.

  1. theorem OAI.Ostmann.primeProgressionTheta_one line 18
  2. theorem OAI.Ostmann.PublishedProgressionInput.principal_theta_bound line 23
  3. theorem OAI.Ostmann.prime_power_error_log_scale line 32
  4. theorem OAI.Ostmann.PublishedProgressionInput.principal_chebyshev_pnt line 56
  5. theorem OAI.Ostmann.PublishedProgressionInput.smoothPrincipalPNT line 77