OAI/NumberTheory/CubicGram/PoissonBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Poisson numerical estimates and local-to-global sieve bounds.

  1. lemma OAI.CubicFirstMoment.poisson_power_identity line 15
  2. lemma OAI.CubicFirstMoment.dual_length_neg_power line 23
  3. lemma OAI.CubicFirstMoment.poisson_cross_one line 29
  4. lemma OAI.CubicFirstMoment.poisson_cross_two line 38
  5. lemma OAI.CubicFirstMoment.poisson_dual_numerical line 49
  6. lemma OAI.CubicFirstMoment.finiteCubicBound_split line 118
  7. lemma OAI.CubicFirstMoment.finiteCubicBound_base_dyad line 133
  8. lemma OAI.CubicFirstMoment.finiteCubicBound_base_global line 162
  9. theorem OAI.CubicFirstMoment.sieveExponent_two line 221
  10. lemma OAI.CubicFirstMoment.finiteCubicBound_empty line 248
  11. lemma OAI.CubicFirstMoment.finiteCubicBound_local_to_global line 254
  12. lemma OAI.CubicFirstMoment.cutoff_log_small_power line 322