OAI/NumberTheory/TotientAsymptotic/FixedCoordinateCenters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform comparison of the two coordinate centers with the order of choices needed in the application: fix the terminal truncation, then the retained range, then let the main endpoint grow.

  1. theorem OAI.TotientAsymptotic.fixed_coordinate_centers_close line 14