OAI/NumberTheory/TotientAsymptotic/IntervalSieveModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A concrete one-dimensional sieve for integers avoiding a prime interval.

  1. def OAI.TotientAsymptotic.intervalSievePrimes line 11
  2. lemma OAI.TotientAsymptotic.mem_intervalSievePrimes line 14
  3. lemma OAI.TotientAsymptotic.intervalSieve_prod_dvd line 18
  4. lemma OAI.TotientAsymptotic.intervalSieve_squarefree line 22
  5. def OAI.TotientAsymptotic.intervalSieveDensity line 26
  6. lemma OAI.TotientAsymptotic.intervalSieveDensity_prime line 29
  7. lemma OAI.TotientAsymptotic.intervalSieveDensity_squarefree line 33
  8. def OAI.TotientAsymptotic.intervalPrimeSieve line 38
  9. lemma OAI.TotientAsymptotic.count_divisible_modulus line 56
  10. lemma OAI.TotientAsymptotic.intervalPrimeSieve_rem_le line 70
  11. lemma OAI.TotientAsymptotic.intervalPrimeSieve_error_sum line 88
  12. def OAI.TotientAsymptotic.intervalSifted line 129
  13. lemma OAI.TotientAsymptotic.intervalSifted_selberg line 132