OAI/NumberTheory/TotientAsymptotic/LocalPrimeSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Each suffix lies in a prime interval determined only by its distance from the end.

  1. def OAI.TotientAsymptotic.localPrimeHeight line 12
  2. lemma OAI.TotientAsymptotic.localPrimeHeight_ge_two line 15
  3. lemma OAI.TotientAsymptotic.localPrimeHeight_mono line 22
  4. lemma OAI.TotientAsymptotic.prime_mem_discard_bound_of_coordinate line 30
  5. theorem OAI.TotientAsymptotic.local_prime_suffix_support line 43
  6. lemma OAI.TotientAsymptotic.localPrimeHeight_log_bound line 63