OAI/NumberTheory/TotientAsymptotic/LocalBadCover.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A failed candidate either fails at its original head or has a bad suffix of its tail. The latter event is independent of the original head.

  1. lemma OAI.TotientAsymptotic.candidatePrimeAt_suffix line 15
  2. theorem OAI.TotientAsymptotic.candidate_bad_suffix line 29
  3. def OAI.TotientAsymptotic.localOriginalBad line 65
  4. def OAI.TotientAsymptotic.localBadSuffixTuples line 68
  5. theorem OAI.TotientAsymptotic.local_bad_candidate_count_cover line 73