OAI/NumberTheory/CubicGram/SieveImprovement.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Amplification, iteration to exponent four-thirds and the cubic large sieve.

  1. def OAI.CubicFirstMoment.sieveImprove line 13
  2. def OAI.CubicFirstMoment.sieveAmplify line 14
  3. lemma OAI.CubicFirstMoment.sieveImprove_properties line 16
  4. lemma OAI.CubicFirstMoment.sieve_amplification_numerical line 37
  5. lemma OAI.CubicFirstMoment.sieve_amplification_size line 74
  6. lemma OAI.CubicFirstMoment.SieveExponent.improve line 102
  7. lemma OAI.CubicFirstMoment.SieveExponent.contract line 149
  8. lemma OAI.CubicFirstMoment.sieveExponent_approach line 163
  9. theorem OAI.CubicFirstMoment.sieveExponent_four_thirds line 177
  10. lemma OAI.CubicFirstMoment.small_four_thirds_le_mixed line 210
  11. theorem OAI.CubicFirstMoment.finiteCubicBound_sharp line 218
  12. def OAI.CubicFirstMoment.squarefreePrimaryBall line 254
  13. lemma OAI.CubicFirstMoment.mem_squarefreePrimaryBall line 257
  14. def OAI.CubicFirstMoment.cubicSieveMass line 264
  15. def OAI.CubicFirstMoment.CubicLargeSieveStatement line 268
  16. theorem OAI.CubicFirstMoment.cubicLargeSieve line 274