OAI/NumberTheory/TotientAsymptotic/NaturalShiftScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The shift at a fixed distance below m(x) has the correct geometric scale.

  1. theorem OAI.TotientAsymptotic.natural_shift_scale_lower line 12
  2. theorem OAI.TotientAsymptotic.natural_contracted_coordinate_lower line 42