OAI/NumberTheory/CubicMoment/Theta/CubicThetaEnergyRegularDomain.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The energy inverse is analytic off the positive real spectral ray, and meromorphic across its part strictly below the cusp threshold two.

  1. lemma OAI.CubicFirstMoment.cubicThetaEnergyMass_positive line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaEnergyMass_norm line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaEnergyPencil_unit line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaEnergyInverse_analytic line 24
  5. theorem OAI.CubicFirstMoment.cubicThetaEnergyInverse_meromorphic line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaEnergyPencil_eventually_unit line 44