OAI/NumberTheory/Ostmann/Supply/MultiplierWeightedBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Elementary divisor and logarithmic budgets for sieve multipliers

  1. def OAI.Ostmann.positiveMultipliers line 10
  2. theorem OAI.Ostmann.positiveMultipliers_card line 12
  3. theorem OAI.Ostmann.positiveMultipliers_dvd_card line 15
  4. def OAI.Ostmann.multiplierPrimeWeight line 26
  5. theorem OAI.Ostmann.multiplierPrimeWeight_nonneg line 29
  6. theorem OAI.Ostmann.multiplierPrimeWeight_total_le line 37
  7. def OAI.Ostmann.badDivisorMultipliers line 53
  8. theorem OAI.Ostmann.badDivisorMultipliers_card_le line 56
  9. def OAI.Ostmann.largeWeightMultipliers line 71
  10. theorem OAI.Ostmann.largeWeightMultipliers_card_budget line 75