OAI/NumberTheory/TotientAsymptotic/DistinctPrimeTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Two nested prime-pair tails, with the larger-prime coefficient allowed to depend on the smaller prime as in Ford's distinct-largest-prime case.

  1. lemma OAI.TotientAsymptotic.two_prime_fiber_sum line 11
  2. lemma OAI.TotientAsymptotic.nested_prime_pair_tail line 21
  3. theorem OAI.TotientAsymptotic.distinct_prime_reciprocal_tail line 61