OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailPoissonCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A concrete dyadic cutoff lying inside the small-conductor range, with a fixed power gap past the natural small-B Poisson scale.

  1. lemma OAI.CubicFirstMoment.primeGroupTail_poisson_cutoff line 10
  2. lemma OAI.CubicFirstMoment.primeGroupTail_poisson_cutoff_scale line 25