OAI/NumberTheory/TotientAsymptotic/CofactorSieveCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A logarithmic endpoint for the cofactor prime-pair sieve.

  1. lemma OAI.TotientAsymptotic.floor_log_endpoint line 10
  2. lemma OAI.TotientAsymptotic.cofactor_sieve_cutoff_mass line 25