OAI/NumberTheory/CubicMoment/Theta/CubicThetaFinitePrimaryProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite projection selected by the actual primary-unit cubic weight. Its image and its relation to Kloosterman energy are exact.

  1. def OAI.CubicFirstMoment.cubicThetaPrimaryMultiplier line 13
  2. def OAI.CubicFirstMoment.cubicThetaFinitePrimaryProjection line 17
  3. theorem OAI.CubicFirstMoment.cubicThetaFinitePrimaryProjection_fourier line 24
  4. theorem OAI.CubicFirstMoment.cubicThetaFinitePrimaryProjection_idempotent line 36
  5. theorem OAI.CubicFirstMoment.cubicThetaFinitePrimaryProjection_fixed_iff line 45
  6. theorem OAI.CubicFirstMoment.cubicThetaFinitePrimaryProjection_energy line 64
  7. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloostermanApply_projection_energy line 78