OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootCriticalSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity and the actual Hecke overlap force the missing square frequency to vanish for the arithmetic residue.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidue_square_projection_zero line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidue_unit_correlation line 35