OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailPoissonAnnulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every finite Poisson annulus, with arbitrary squarefree coefficients, in the small-B range. No restriction on the translated arithmetic height.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_poisson_annulus_height_power line 13