OAI/NumberTheory/CubicMoment/Estimates/NormMellinMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrated decay with polynomial Mellin-height weights. This controls truncated shifts in the dispersion kernel.

  1. theorem OAI.CubicFirstMoment.normDenominatorMellinCoefficient_moment_decay line 12
  2. lemma OAI.CubicFirstMoment.mellin_window_majorant line 47
  3. theorem OAI.CubicFirstMoment.integral_schwartz_window line 61