OAI/NumberTheory/CubicMoment/Theta/CubicThetaResidueSourceOrbit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual residue applied to the full positive-cutoff source orbit. The scalar recurrence here is derived from its proved Hecke eigenvalue.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmeticResidueL2_hecke line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaResidueSourcePairing_hecke line 20
  3. def OAI.CubicFirstMoment.cubicThetaPrimeResidueOrbit line 27
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeResidueOrbit_step line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeResidueOrbit_square_start line 56
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeResidueOrbit_square_closed line 65