OAI/NumberTheory/CubicMoment/Theta/CubicThetaDirichletIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute interchange for the actual frequency Dirichlet series along a vertical line. This will be applied to the dual series on a far-left Mellin contour, where its argument has real part greater than two.

  1. theorem OAI.CubicFirstMoment.cubicThetaDirichlet_integral_summable line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaDirichlet_integral line 37