OAI/NumberTheory/TotientAsymptotic/TailProductBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The capped tail has the subpower denominator required by the prime window.

  1. lemma OAI.TotientAsymptotic.prime_tail_log_bound line 11
  2. lemma OAI.TotientAsymptotic.capped_tail_denominator_budget line 24
  3. lemma OAI.TotientAsymptotic.capped_prime_tail_denominator line 51