OAI/NumberTheory/TotientAsymptotic/IntervalSieveDenominator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The interval sieve has the reciprocal Euler-product denominator.

  1. def OAI.TotientAsymptotic.intervalSieveWeight line 13
  2. lemma OAI.TotientAsymptotic.intervalSieveWeight_nonneg line 15
  3. lemma OAI.TotientAsymptotic.intervalSieveWeight_density line 20
  4. lemma OAI.TotientAsymptotic.intervalSieveWeight_moment line 27
  5. lemma OAI.TotientAsymptotic.intervalSieve_moment_le line 40
  6. lemma OAI.TotientAsymptotic.intervalSieveTerms_prod line 59
  7. lemma OAI.TotientAsymptotic.intervalSieveBoundingSum_powerset line 74
  8. theorem OAI.TotientAsymptotic.intervalSieveBoundingSum_lower line 94