OAI/NumberTheory/TotientAsymptotic/DistinctPrimeMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal mass after extracting the two unequal largest primes.

  1. abbrev OAI.TotientAsymptotic.TwoPrimeEncoding line 11
  2. def OAI.TotientAsymptotic.twoPrimeWeight line 13
  3. def OAI.TotientAsymptotic.distinctCoefficient line 16
  4. structure OAI.TotientAsymptotic.DistinctPrimeWitness line 19
  5. lemma OAI.TotientAsymptotic.distinct_prime_fiber_sum line 32
  6. lemma OAI.TotientAsymptotic.distinct_prime_fiber_bound line 47
  7. theorem OAI.TotientAsymptotic.distinct_prime_squarefree_mass_bound line 78