OAI/NumberTheory/TotientAsymptotic/CollisionScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete renewal bounds needed for the manuscript's collision cutoff. These are proved from the defining series; no additional numerical input is assumed.

  1. lemma OAI.TotientAsymptotic.small_log_identities line 14
  2. lemma OAI.TotientAsymptotic.log_seven_bounds line 22
  3. lemma OAI.TotientAsymptotic.renewal_tail_majorant line 32
  4. lemma OAI.TotientAsymptotic.renewalSeries_thirteen_twentyfifths_lt_one line 54
  5. lemma OAI.TotientAsymptotic.renewalSeries_onehundredthirtyseven_twohundredfiftieths_gt_one line 72
  6. lemma OAI.TotientAsymptotic.collision_rho_bounds line 86
  7. lemma OAI.TotientAsymptotic.collision_lambda_bounds line 101