OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalEnergyResolvent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The local candidate inverse at an exceptional real parameter is an analytic inverse on the complementary subspace plus an explicit simple pole on the finite exceptional space. Algebraic agreement with the original inverse is proved separately.

  1. def OAI.CubicFirstMoment.cubicThetaLocalEnergyResolvent line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaEnergyPencil_analytic line 19
  3. theorem OAI.CubicFirstMoment.cubicThetaLocalEnergyResolvent_meromorphic line 31