OAI/NumberTheory/CubicGram/SieveExponent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Quantitative cube and dual bounds under a sieve exponent.

  1. def OAI.CubicFirstMoment.SieveExponent line 16
  2. lemma OAI.CubicFirstMoment.dyadic_polynomial_small_power line 23
  3. lemma OAI.CubicFirstMoment.squarefreePrimaryDyad_card_le line 54
  4. lemma OAI.CubicFirstMoment.cubeDyad_sizes line 58
  5. lemma OAI.CubicFirstMoment.cube_block_scaled line 78
  6. lemma OAI.CubicFirstMoment.cube_scaled_sizes line 88
  7. lemma OAI.CubicFirstMoment.SieveExponent.cube_bound line 93
  8. def OAI.CubicFirstMoment.decayConstant line 197
  9. lemma OAI.CubicFirstMoment.decayConstant_pos line 199
  10. lemma OAI.CubicFirstMoment.finite_polynomial_dyadic_bound line 203
  11. lemma OAI.CubicFirstMoment.SieveExponent.dual_bound line 225