OAI/NumberTheory/TotientAsymptotic/CollisionChoiceCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The remaining finite choices fit inside the recovered collision saving.

  1. lemma OAI.TotientAsymptotic.canceled_mass_power_bound line 11
  2. lemma OAI.TotientAsymptotic.smooth_choice_cost line 34
  3. lemma OAI.TotientAsymptotic.residual_choice_exponent line 53
  4. lemma OAI.TotientAsymptotic.subset_choice_cost line 67
  5. lemma OAI.TotientAsymptotic.rounded_prime_endpoint_height line 77
  6. lemma OAI.TotientAsymptotic.canceled_rounded_mass_power line 103