OAI/NumberTheory/TotientAsymptotic/ComparisonSizes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Integer size and large-prime-part bounds for Ford's comparison hypotheses.

  1. def OAI.TotientAsymptotic.partBelow line 11
  2. lemma OAI.TotientAsymptotic.partBelow_mul_partAbove line 14
  3. lemma OAI.TotientAsymptotic.partBelow_bound line 20
  4. lemma OAI.TotientAsymptotic.smooth_integer_log_bound line 43
  5. lemma OAI.TotientAsymptotic.smooth_integer_size line 54
  6. lemma OAI.TotientAsymptotic.partAbove_log_lower line 63
  7. lemma OAI.TotientAsymptotic.partAbove_gt_sqrt line 77