OAI/NumberTheory/TotientAsymptotic/FordCostBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The published Ford prefactors and tuple recovery fit inside the saving.

  1. lemma OAI.TotientAsymptotic.recovery_log_cost_small line 11
  2. lemma OAI.TotientAsymptotic.smooth_log_cost_small line 25
  3. lemma OAI.TotientAsymptotic.ford_polynomial_prefactor line 47