OAI/NumberTheory/CubicMoment/Estimates/MellinMomentPowers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed powers in the central-plus-tail short-convolution estimate.

  1. lemma OAI.CubicFirstMoment.short_mellin_tail_power line 10
  2. theorem OAI.CubicFirstMoment.absorb_short_mellin_bounds line 27