OAI/NumberTheory/CubicMoment/Transform/MetaplecticRegularGluing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compatible regular numerators for different Mellin test functions. Their compatibility follows by analytic continuation of their literal Dirichlet-series identity in the half-plane of absolute convergence.

  1. def OAI.CubicFirstMoment.metaplecticRegularNumerator line 15
  2. lemma OAI.CubicFirstMoment.metaplecticRegularNumerator_differentiableOn line 19
  3. lemma OAI.CubicFirstMoment.metaplecticRegularNumerator_right line 31
  4. theorem OAI.CubicFirstMoment.metaplecticRegularNumerator_compatible line 49