OAI/NumberTheory/TotientAsymptotic/LocalFullCandidateCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite pruning of the actual candidate family on its original normalization. The regular comparison estimates are kept explicit here for application to Ford's finite labeled counts.

  1. def OAI.TotientAsymptotic.localFullCandidates line 16
  2. def OAI.TotientAsymptotic.LocalOriginalRegularBound line 19
  3. def OAI.TotientAsymptotic.LocalSuffixRegularBound line 26
  4. lemma OAI.TotientAsymptotic.local_candidate_card_partition line 34
  5. theorem OAI.TotientAsymptotic.local_full_candidate_count line 40