OAI/NumberTheory/TotientAsymptotic/LocalRegularReciprocalMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrate an actual regular-residual counting estimate over its occupied layers. Only the fourth inverse power of the local double logarithm is needed.

  1. theorem OAI.TotientAsymptotic.residual_fourth_power_mass line 12
  2. theorem OAI.TotientAsymptotic.local_residual_mass_of_fourth_power_count line 48