OAI/NumberTheory/CubicMoment/Theta/CubicThetaEnergySimplePole.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact residue of the actual energy inverse. The complementary inverse is analytic and the exceptional projection gives a simple pole.

  1. lemma OAI.CubicFirstMoment.cubicThetaProjectedInverse_analytic line 11
  2. lemma OAI.CubicFirstMoment.scale_pole line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyResolvent_scaled line 31
  4. theorem OAI.CubicFirstMoment.cubicThetaEnergyInverse_residue line 43