OAI/NumberTheory/CubicMoment/Angular/AngularHeightDivisorBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual angular common-divisor mass: exact empty row, rough-divisor split, and shortened outer-sieve bound. The constants do not depend on the angular index, since its coefficient factors have modulus one.

  1. def OAI.CubicFirstMoment.angular_fullPrimeDivisorMellinMass line 19
  2. lemma OAI.CubicFirstMoment.angular_fullPrimeDivisorMellinMass_one line 28
  3. lemma OAI.CubicFirstMoment.angular_fullPrimeDivisorMellinMass_small line 39
  4. lemma OAI.CubicFirstMoment.angular_fullPrime_coprime_mass_split line 57
  5. lemma OAI.CubicFirstMoment.angular_fullPrimeDivisorMellinMass_le line 91
  6. theorem OAI.CubicFirstMoment.angular_fullPrime_divisor_outer_mass line 105
  7. theorem OAI.CubicFirstMoment.angular_fullPrime_large_divisor_mass line 144
  8. theorem OAI.CubicFirstMoment.angular_fullPrime_large_divisor_log_saving line 203
  9. theorem OAI.CubicFirstMoment.angular_fullPrime_coprime_mass_integral_le line 272
  10. theorem OAI.CubicFirstMoment.angular_fullPrime_divisor_noncoprime_log_saving line 310