OAI/NumberTheory/Ostmann/Preliminaries/PrimeCoverageWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Converting full prime coverage into a nonnegative pair-weight bound

  1. theorem OAI.Ostmann.covered_weight_sum_le line 10
  2. theorem OAI.Ostmann.smooth_covered_weight_le line 26
  3. theorem OAI.Ostmann.EventuallyPrimeSumset.smooth_coverage line 49