OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalSpectralResolvent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The constructed global Green operator gives the actual Eisenstein spectral resolvent initially in Re(s)>2 and at nonreal points of Re(s)>1. Real poles in (1,2] still require meromorphic continuation.

  1. def OAI.CubicFirstMoment.cubicThetaGlobalSpectralParameter line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaGlobalSpectralParameter_regular line 13
  3. def OAI.CubicFirstMoment.cubicThetaGlobalSpectralResolvent line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaGlobalSpectralResolvent_analytic line 35
  5. theorem OAI.CubicFirstMoment.cubicThetaGlobalSpectralResolvent_weak line 42