OAI/NumberTheory/CubicMoment/Estimates/PrimeCoprimeMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact common-divisor mass for full prime rows. Roughness leaves only the empty divisor below a chosen threshold; every remaining term has a genuinely large common divisor.

  1. def OAI.CubicFirstMoment.fullPrimeDivisorMellinMass line 16
  2. lemma OAI.CubicFirstMoment.fullPrimeDivisorMellinMass_one line 25
  3. lemma OAI.CubicFirstMoment.fullPrimeDivisorMellinMass_small line 33
  4. lemma OAI.CubicFirstMoment.fullPrime_coprime_mass_split line 51