OAI/NumberTheory/TwoPoint/Bounds/QualitativePrimeScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The published Mertens estimate on the smaller qualitative sieve cutoff, and the exact inclusion of its primes in the roughness condition.

  1. def OAI.TwoPointCorrelations.qualitativeSievePrimes line 14
  2. def OAI.TwoPointCorrelations.HasNoPrimeFactorBelow line 17
  3. lemma OAI.TwoPointCorrelations.qualitativeSieveLogCutoff_lt_power line 20
  4. lemma OAI.TwoPointCorrelations.HasNoPrimeFactorBelow.qualitativeSieve line 27
  5. theorem OAI.TwoPointCorrelations.PrimeReciprocalInput.qualitative_scale line 35