OAI/NumberTheory/CubicMoment/Estimates/MellinFiniteSeminorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite seminorm control of vertical Mellin transforms. This keeps the cost of a varying smooth cutoff visible instead of hiding it in a constant.

  1. lemma OAI.CubicFirstMoment.mellinLogSchwartz_seminorm_cost line 12
  2. def OAI.CubicFirstMoment.mellinVerticalCLM line 82
  3. theorem OAI.CubicFirstMoment.mellinVertical_finite_seminorm line 88