OAI/NumberTheory/TotientAsymptotic/IntervalPrimeMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform reciprocal-prime mass in the intervals used for normality.

  1. lemma OAI.TotientAsymptotic.primesUpTo_mem line 10
  2. lemma OAI.TotientAsymptotic.prime_interval_sum_eq line 19
  3. lemma OAI.TotientAsymptotic.primeReciprocalLE_bounded_error line 45