OAI/NumberTheory/TotientAsymptotic/CoordinateExponentialCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential form of the weighted-coordinate count. The hypotheses record only numerical budgets, so the dimension and the excess may vary with X.

  1. lemma OAI.TotientAsymptotic.coordinate_grid_prefactor line 12
  2. theorem OAI.TotientAsymptotic.coordinate_exponential_count line 20