OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimePairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of an original section and a prime Atkin translate. The cancellation is an actual integral on the common finite cover.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeSectionPair_invariant line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinConjugate_kubota line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeOriginalAtkinPair_translate line 33
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeOriginalAtkinPair_integral_zero line 57