OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramCubeLowerLayers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The lower denominator layers of the actual Gram kernel at two cubically multiplied frequencies.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeIndex_zero line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_cube_layer_one line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_cube_layer_two line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaFiniteKloosterman_cube_unit line 39
  5. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_cube_layer_three line 53