OAI/NumberTheory/TotientAsymptotic/IntervalSieveEuler.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An interval Euler-product lower bound from the already proved Mertens bound.

  1. lemma OAI.TotientAsymptotic.intervalSieveWeight_euler line 13
  2. lemma OAI.TotientAsymptotic.primeEulerProduct_interval line 21
  3. theorem OAI.TotientAsymptotic.intervalSieveEuler_lower line 50
  4. theorem OAI.TotientAsymptotic.intervalSifted_bound line 68