OAI/NumberTheory/CubicMoment/Estimates/HeightCoprimeDispersion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The averaged estimate for the original coprime Gram form, obtained from the complete Poisson series without omitting any frequencies.

  1. theorem OAI.CubicFirstMoment.height_coprime_dispersion_saving line 13