OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanZeroIndices.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact zero-phase factors at the first three prime powers. These are used for the lower layers when both Gram frequencies contain a cube.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeKloosterman_multiple line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_zero_indices line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_prime_origin line 30
  4. lemma OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_square_zero line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_cube_zero line 50