OAI/NumberTheory/CubicMoment/Transform/MetaplecticRegularMellin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A regularized Mellin transform built from the actual Voronoi sum. The smooth subtraction vanishes near zero and agrees exactly with the published main term for large scale. No continuation is assumed.

  1. def OAI.CubicFirstMoment.metaplecticRegularScale line 16
  2. lemma OAI.CubicFirstMoment.metaplecticMain_zero_mode line 20
  3. lemma OAI.CubicFirstMoment.continuousOn_metaplecticRegularScale line 26
  4. lemma OAI.CubicFirstMoment.metaplecticRegularScale_zero_near_zero line 38
  5. lemma OAI.CubicFirstMoment.metaplecticRegularScale_decay line 60
  6. lemma OAI.CubicFirstMoment.metaplecticRegularMellin_differentiableOn line 80
  7. lemma OAI.CubicFirstMoment.metaplecticRegularMellin_convergent line 101