OAI/NumberTheory/TotientAsymptotic/SmallIntervalPart.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The interval part in Ford 4.1 is small enough for the quotient sieve.

  1. lemma OAI.TotientAsymptotic.partBetween_le_partBelow line 9
  2. lemma OAI.TotientAsymptotic.interval_part_log_bound line 15
  3. lemma OAI.TotientAsymptotic.interval_part_sieve_size line 25
  4. lemma OAI.TotientAsymptotic.ford_interval_part_sieve_size line 41