OAI/NumberTheory/TotientAsymptotic/EnlargementTail.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two perturbations used for full prime boxes have summable weighted cost, including after multiplication by the smooth-cofactor envelope.

  1. def OAI.TotientAsymptotic.simplexBoxError line 15
  2. def OAI.TotientAsymptotic.simplexBoxTail line 18
  3. lemma OAI.TotientAsymptotic.simplexBoxError_nonneg line 22
  4. lemma OAI.TotientAsymptotic.simplexBoxError_weighted line 28
  5. lemma OAI.TotientAsymptotic.summable_simplexBoxError_weighted line 35
  6. lemma OAI.TotientAsymptotic.simplexBoxTail_eq_tsum line 45
  7. lemma OAI.TotientAsymptotic.simplexBoxTail_tendsto line 61
  8. lemma OAI.TotientAsymptotic.cofactor_simplexBoxTail_tendsto line 69