OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFourierPairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact nonzero-frequency test duality for the actual Hecke operator.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeFourierPairing_finite line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeFourierPairing_energy line 86