OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticPoleIsolation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic family has an analytic germ throughout Re(s)>1, except for its already proved nonzero pole at 4/3. The representative supplied by the inverse operator can differ at an isolated singular parameter.

  1. lemma OAI.CubicFirstMoment.analytic_apply line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaForcedEnergy_analytic_regular line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaForcedResolvent_analytic_regular line 34
  4. theorem OAI.CubicFirstMoment.cubicThetaForcedEnergy_analytic_germ line 39
  5. theorem OAI.CubicFirstMoment.cubicThetaForcedResolvent_analytic_germ line 51