OAI/NumberTheory/CubicMoment/Angular/AngularHeightCoprimeIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full-line Mellin and independent height averaging for the actual coprime Poisson mass. Every nonzero frequency and every common divisor are included. The published hypotheses enter through the empty row.

  1. theorem OAI.CubicFirstMoment.angular_height_coprime_mellin_saving line 20