OAI/NumberTheory/TotientAsymptotic/TripleSieveModel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete Selberg sieve for q, aq+1 and bq+1.

  1. def OAI.TotientAsymptotic.tripleSievePrimes line 11
  2. lemma OAI.TotientAsymptotic.mem_tripleSievePrimes line 13
  3. lemma OAI.TotientAsymptotic.tripleSievePrimes_squarefree line 17
  4. lemma OAI.TotientAsymptotic.mem_tripleSievePrimes_of_dvd line 27
  5. def OAI.TotientAsymptotic.tripleSieveDensity line 33
  6. lemma OAI.TotientAsymptotic.tripleSieveDensity_prime line 36
  7. lemma OAI.TotientAsymptotic.tripleSieveDensity_positive line 40
  8. lemma OAI.TotientAsymptotic.tripleSieveDensity_lt_one line 48
  9. lemma OAI.TotientAsymptotic.tripleSievePolynomial_strictMono line 55
  10. def OAI.TotientAsymptotic.triplePrimeSieve line 66