OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanUnitScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact unit change of variables in the actual Kloosterman kernel. The multiplier is the cubic character from the Eisenstein row weight.

  1. theorem OAI.CubicFirstMoment.cubicThetaFiniteKloosterman_unit_scale line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_unit_scale line 45