OAI/NumberTheory/CubicMoment/Theta/CubicThetaNonzeroSpectralResidue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit arithmetic constant term forces a nonzero residue of the actual global meromorphic family at s=4/3.

  1. lemma OAI.CubicFirstMoment.cubicThetaScatteringResidue_ne_zero line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSpectralResidue_constant_ne_zero line 18
  3. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidueEnergy_ne_zero line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspRestriction_value_bound line 38
  5. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidueValue_ne_zero line 56