OAI/NumberTheory/CubicMoment/Theta/CubicThetaPoincarePairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cubic multiplier cancels in the pairing of a periodized seed with an actual automorphic section. The resulting sum is locally finite.

  1. lemma OAI.CubicFirstMoment.cubicThetaPoincare_pairing_point line 13