OAI/NumberTheory/CubicMoment/Theta/CubicThetaKloostermanCubeInflation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing a common cubic prime factor from the actual local Kloosterman kernel. The quotient map retains the inverse term and the zero extension.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerReduction_cube_inverse line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerWeight_cube line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_cubeInflation line 47
  4. theorem OAI.CubicFirstMoment.cubicThetaSymbolKloosterman_cubeInflation_residue line 82