OAI/NumberTheory/TotientAsymptotic/CollisionChoiceBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Prime and smoothness bounds for all the choices in the class partition.

  1. lemma OAI.TotientAsymptotic.wholeWitnessPrime_prime line 12
  2. lemma OAI.TotientAsymptotic.witnessBlockValue_pos line 20
  3. lemma OAI.TotientAsymptotic.whole_shift_le_block line 28
  4. lemma OAI.TotientAsymptotic.canceledPrimesAt_prime_bound line 37