OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeSquareFourier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At a frequency with prime valuation exactly two, both cubic-character branches cancel and the dilation branch is absent.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstKernel_multiple line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeSecondKernel_multiple line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrime_cube_not_dvd_square line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHecke_fourier_square line 32