OAI/NumberTheory/TotientAsymptotic/LocalSuffixAggregation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert a reciprocal bound for each actual bad suffix family to the count of original candidates, summing over all possible removed prefixes.

  1. theorem OAI.TotientAsymptotic.local_suffix_count_aggregation_mul line 14
  2. theorem OAI.TotientAsymptotic.local_suffix_count_aggregation line 82