OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierPoleIsolation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The continued arithmetic Fourier coefficient has no artificial poles from the initial fixed radial test. Its only possible pole in Re(s)>1 is the actual arithmetic pole at 4/3.

  1. theorem OAI.CubicFirstMoment.cubicThetaFrequencyContinuation_analytic_germ line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaFrequencyContinuation_principal_part line 44