OAI/NumberTheory/TotientAsymptotic/BootstrapResidualSize.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

After two leading primes, a surviving preimage has a subpower residual.

  1. lemma OAI.TotientAsymptotic.fordCofactor_le_power line 12
  2. lemma OAI.TotientAsymptotic.fordCofactor_log_le line 39
  3. lemma OAI.TotientAsymptotic.bootstrap_factor_scale line 45
  4. theorem OAI.TotientAsymptotic.bootstrap_cofactor_size line 67
  5. theorem OAI.TotientAsymptotic.bootstrap_residual_size line 99