OAI/NumberTheory/TotientAsymptotic/GeometricLowerBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two numerical margins needed for the inner prime grid.

  1. lemma OAI.TotientAsymptotic.geometric_dominates_polynomial line 11
  2. lemma OAI.TotientAsymptotic.ambient_polynomial_budget line 24