OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeArithmeticResidue.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The nonzero arithmetic spectral residue is lifted to the actual prime cover. Its Atkin translate has equal norm and is orthogonal to it.

  1. def OAI.CubicFirstMoment.cubicThetaArithmeticResidueL2 line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticResidueL2_ne_zero line 16
  3. def OAI.CubicFirstMoment.cubicThetaPrimeArithmeticResidue line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeArithmeticResidue_ne_zero line 24
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeArithmeticResidue_orthogonal line 31
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeArithmeticResidue_norm line 36