OAI/NumberTheory/CubicMoment/Theta/CubicThetaAdditiveMellin.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Identify the initial Dirichlet series of each rationally shifted theta function before using its continued Mellin expression.

  1. def OAI.CubicFirstMoment.cubicThetaAdditiveCoefficient line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaAdditiveCoefficient_norm line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaAdditiveCoefficient_term line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaAdditiveCoefficient_series line 29
  5. theorem OAI.CubicFirstMoment.cubicThetaAdditive_mellin line 35
  6. theorem OAI.CubicFirstMoment.cubicThetaLevelCompleted_dirichlet line 41