OAI/NumberTheory/CubicMoment/Angular/AngularHeightAllFrequencyMellin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full-line Mellin transfer of every nonzero height-averaged frequency. The arithmetic height interval and the Mellin variable are independent.

  1. theorem OAI.CubicFirstMoment.angular_height_all_frequency_mellin_saving line 17