OAI/NumberTheory/CubicMoment/Transform/MetaplecticWeightedContinuation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A holomorphic regular part for the completed Dirichlet series multiplied by the Mellin transform of any compact smooth test function. It is constructed from the literal Voronoi asymptotic.

  1. def OAI.CubicFirstMoment.metaplecticWeightedRegular line 15
  2. lemma OAI.CubicFirstMoment.metaplecticWeightedRegular_differentiableOn line 19
  3. theorem OAI.CubicFirstMoment.metaplecticWeightedRegular_eq line 28