OAI/NumberTheory/CubicMoment/Theta/CubicThetaPositiveZeroWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The zero Fourier mode at every positive cutoff. The incoming Mellin term is entire and therefore contributes no residue.

  1. lemma OAI.CubicFirstMoment.cubicThetaFullTorus_zero line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaEisenstein_horizontal_zero line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaPositiveZeroObservable_normalized line 39
  4. theorem OAI.CubicFirstMoment.cubicThetaPositiveZeroObservable_continued line 70
  5. theorem OAI.CubicFirstMoment.cubicThetaPositiveResidue_zero_observation line 95