OAI/NumberTheory/TotientAsymptotic/CollisionSieveTails.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Height-uniform reciprocal sieve bounds for the two collision branches.

  1. lemma OAI.TotientAsymptotic.tripleDiscriminant_le_cube line 11
  2. lemma OAI.TotientAsymptotic.B_cube line 22
  3. lemma OAI.TotientAsymptotic.cube_exp_two line 28
  4. theorem OAI.TotientAsymptotic.collision_triple_reciprocal_tail line 35
  5. theorem OAI.TotientAsymptotic.collision_pair_reciprocal_tail line 65
  6. theorem OAI.TotientAsymptotic.collision_triple_reciprocal_tail_ne line 82