OAI/NumberTheory/TotientAsymptotic/LocalSuffixRegular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the finite regular comparison count to the actual distinct suffix values, then integrate their occupied dyadic layers.

  1. theorem OAI.TotientAsymptotic.local_suffix_regular_bound line 16