OAI/NumberTheory/CubicMoment/Estimates/MellinHeightTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rapid Mellin truncation with an explicit integrable moment.

  1. lemma OAI.CubicFirstMoment.outside_interval_abs line 11
  2. lemma OAI.CubicFirstMoment.weighted_height_tail line 16
  3. lemma OAI.CubicFirstMoment.bounded_product_height_tail line 28
  4. theorem OAI.CubicFirstMoment.zeroLineMellinWeight_moment_integrable line 46
  5. lemma OAI.CubicFirstMoment.zeroLineMellinWeight_moment line 60