OAI/NumberTheory/CubicMoment/Estimates/SmallPrimeParts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual small-prime partition of squarefree cubic moduli. Its parts divide the small modulus, so their number has a proved subpower bound.

  1. def OAI.CubicFirstMoment.supportedIdealPart line 13
  2. def OAI.CubicFirstMoment.outsideIdealPart line 16
  3. lemma OAI.CubicFirstMoment.supported_add_outside line 19
  4. lemma OAI.CubicFirstMoment.supportedIdealPart_le line 22
  5. lemma OAI.CubicFirstMoment.outsideIdealPart_le line 28
  6. def OAI.CubicFirstMoment.primarySmallPart line 34
  7. def OAI.CubicFirstMoment.primaryOutsidePart line 37
  8. lemma OAI.CubicFirstMoment.primarySmallPart_primary line 40
  9. lemma OAI.CubicFirstMoment.primaryOutsidePart_primary line 43
  10. lemma OAI.CubicFirstMoment.primary_small_outside_mul line 46
  11. lemma OAI.CubicFirstMoment.primarySmallPart_dvd line 53
  12. lemma OAI.CubicFirstMoment.primaryOutsidePart_coprime line 65
  13. lemma OAI.CubicFirstMoment.primarySmallPart_squarefree line 79
  14. lemma OAI.CubicFirstMoment.primaryOutsidePart_squarefree line 86
  15. theorem OAI.CubicFirstMoment.smallPrimeParts_card line 93