OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRadialPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact compact radial test duality for the actual Hecke operator, first on finite-energy sections and then by density.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCube_height_ge_one line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRadialWeight_low line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRadialPairing_finite line 29
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRadialPairing_energy line 83