OAI/NumberTheory/CubicMoment/Angular/AngularHeightCoprimeDispersion.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.angular_height_coprime_dispersion_saving line 15