OAI/NumberTheory/TotientAsymptotic/SubpowerCandidate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The candidate tail is smaller than every fixed power of the ambient scale.

  1. lemma OAI.TotientAsymptotic.subpower_log_eventually_le line 11
  2. lemma OAI.TotientAsymptotic.capped_tail_subpower line 17
  3. lemma OAI.TotientAsymptotic.subpower_head_lower line 37