OAI/NumberTheory/CubicMoment/Theta/CubicThetaSmoothMellin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Mellin inversion for the literal arithmetic frequency coefficients. The coefficient carries one frequency norm, so its Dirichlet variable is 2*s-1, exactly as in the theta Gamma completion.

  1. lemma OAI.CubicFirstMoment.cubicThetaDirichlet_nonzero line 15
  2. lemma OAI.CubicFirstMoment.cubicTheta_norm_square_power line 28
  3. lemma OAI.CubicFirstMoment.cubicTheta_norm_square_weight line 39
  4. lemma OAI.CubicFirstMoment.cubicTheta_normDirichlet line 46
  5. theorem OAI.CubicFirstMoment.cubicTheta_smooth_mellin line 57
  6. lemma OAI.CubicFirstMoment.cubicThetaAdditive_angular_norm line 82
  7. theorem OAI.CubicFirstMoment.cubicThetaAngular_smooth_continued line 95