OAI/NumberTheory/CubicMoment/Estimates/MellinStrip.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform rapid Mellin decay on a fixed closed real strip. The bound comes from the actual compact logarithmic support, not an additional analytic input.

  1. lemma OAI.CubicFirstMoment.exp_linear_deriv_bound line 16
  2. lemma OAI.CubicFirstMoment.mellinLogSchwartz_eq_smul line 30
  3. theorem OAI.CubicFirstMoment.mellinLogSchwartz_seminorm_uniform line 37
  4. theorem OAI.CubicFirstMoment.mellinVertical_family_bounded line 86
  5. theorem OAI.CubicFirstMoment.smooth_mellin_strip_decay line 105