OAI/NumberTheory/Ostmann/ZeroDensity/ActualProgressionInput.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The prime-progression estimate with constructed exceptional zeros

This is the theta estimate of Montgomery–Vaughan, Corollary 11.20. The actual exceptional-zero family records divisibility, completeness and Page uniqueness.

  1. def OAI.Ostmann.ActualProgressionTheta line 13
  2. def OAI.Ostmann.progressionInput_of_actual_theta line 21