OAI/NumberTheory/CubicMoment/Theta/CubicThetaFrequencyContinuation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Meromorphic continuation of the literal nonzero arithmetic Fourier Dirichlet coefficients, obtained from the actual automorphic resolvent.

  1. lemma OAI.CubicFirstMoment.cubicThetaRadialTest_eventually_ne_zero line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaGamma_analytic_right line 23
  3. def OAI.CubicFirstMoment.cubicThetaFrequencyQuotient line 35
  4. lemma OAI.CubicFirstMoment.cubicThetaFrequencyQuotient_meromorphic line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaFrequencyQuotient_right line 46
  6. def OAI.CubicFirstMoment.cubicThetaFrequencyContinuation line 55
  7. theorem OAI.CubicFirstMoment.cubicThetaFrequencyContinuation_right line 58
  8. theorem OAI.CubicFirstMoment.cubicThetaFrequencyContinuation_meromorphic line 62