OAI/NumberTheory/CubicMoment/Theta/CubicThetaSpectralSimplePole.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the simple energy pole to the Eisenstein parameter. The derivative factor is explicit and nonzero on the real interval (1,2).

  1. lemma OAI.CubicFirstMoment.cubicThetaSpectralParameter_gap line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSpectralParameter_punctured line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaRealSpectralParameter_range line 40
  4. lemma OAI.CubicFirstMoment.cubicThetaRealSpectralParameter_closedRange line 46
  5. lemma OAI.CubicFirstMoment.spectral_rescale line 52
  6. lemma OAI.CubicFirstMoment.rescale_associative line 64
  7. theorem OAI.CubicFirstMoment.cubicThetaSpectralEnergyInverse_residue_closed line 67
  8. theorem OAI.CubicFirstMoment.cubicThetaSpectralEnergyInverse_residue line 115