OAI/NumberTheory/TotientAsymptotic/SecondPrimeBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

All nonleading prime coordinates lie below the ambient log-log scale.

  1. lemma OAI.TotientAsymptotic.ford_second_prime_sq_le line 12
  2. lemma OAI.TotientAsymptotic.all_preimages_square_bound line 19
  3. lemma OAI.TotientAsymptotic.all_preimages_second_coordinate line 43