OAI/NumberTheory/CubicMoment/Estimates/PrimeExclusionLog.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic, rather than merely subpower, number of prime exclusions. This is necessary when the free prime is exp(sqrt(log X)).

  1. theorem OAI.CubicFirstMoment.primary_prime_divisor_card_log line 13
  2. theorem OAI.CubicFirstMoment.prime_exclusion_logarithmic line 36
  3. theorem OAI.CubicFirstMoment.prime_exclusion_polynomial_norm line 51