OAI/NumberTheory/CubicMoment/Theta/CubicThetaMellinReciprocity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Mellin continuation of the actual arithmetic theta expansion. The undetermined constant-to-Fourier ratio remains visible in both residues.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticAxis line 12
  2. def OAI.CubicFirstMoment.cubicThetaArithmeticTail line 15
  3. def OAI.CubicFirstMoment.cubicThetaArithmeticCompleted line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaArithmeticAxis_small line 22
  5. lemma OAI.CubicFirstMoment.cubicThetaArithmeticAxis_decomposition line 34
  6. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCompleted_mellin line 55
  7. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCompleted_even line 87
  8. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCompleted_dirichlet line 94