OAI/NumberTheory/CubicMoment/Estimates/FullMellinMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joining the central Mellin moment to a proved rapid tail bound.

  1. lemma OAI.CubicFirstMoment.norm_square_le_central_tail line 11
  2. theorem OAI.CubicFirstMoment.full_mellin_moment_of_central line 22