OAI/NumberTheory/TotientAsymptotic/CoordinateEnlargement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Away from the terminal coordinates, the diagonal enlargement is uniformly close to one. At fixed truncation the additive budget correction vanishes.

  1. def OAI.TotientAsymptotic.coordinateEnlargement line 13
  2. lemma OAI.TotientAsymptotic.coordinateEnlargement_one_le line 16
  3. theorem OAI.TotientAsymptotic.coordinateEnlargement_close line 22
  4. theorem OAI.TotientAsymptotic.fixed_coordinate_budget_small line 36