OAI/NumberTheory/TotientAsymptotic/PrimeIntervalMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Endpoint bookkeeping for reciprocal primes in half-open intervals.

  1. def OAI.TotientAsymptotic.primesUpTo line 11
  2. def OAI.TotientAsymptotic.primesBelow line 14
  3. def OAI.TotientAsymptotic.primeReciprocalLE line 17
  4. def OAI.TotientAsymptotic.primeReciprocalLT line 19
  5. lemma OAI.TotientAsymptotic.mem_primesUpTo line 21
  6. lemma OAI.TotientAsymptotic.mem_primesBelow line 30
  7. lemma OAI.TotientAsymptotic.primeReciprocal_endpoint_error line 35
  8. lemma OAI.TotientAsymptotic.unitPrimeBox_reciprocal line 65