OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailCoprimeDispersion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The arbitrary-coefficient small-B estimate for the original coprime dispersion Gram form, obtained from the complete Poisson series.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_coprime_dispersion_height_power line 12