OAI/NumberTheory/TotientAsymptotic/AllShiftedPrimePairs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restoring the small primes removed by the sieve cutoff.

  1. def OAI.TotientAsymptotic.allShiftedPrimePairs line 10
  2. lemma OAI.TotientAsymptotic.allShiftedPrimePairs_card_le line 13
  3. lemma OAI.TotientAsymptotic.allShiftedPrimePairs_cutoff line 18
  4. lemma OAI.TotientAsymptotic.totient_ratio_one_le line 34