OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFourierKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unit-branch Fourier kernels, with their actual zero extension. The passage from units to all residues is valid precisely for the two positive cubic powers occurring in the Hecke correspondence.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeCharacter_representative line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeCharacter_nonunit line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeGauss_units line 32
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitFourier line 56
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitFourier_eq line 63
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitFourier_zero line 74
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUnitFourier_reduction line 80